Advertisement

Compositional Verification: Decidability Issues Using Graph Substitutions

  • Olivier Ly
Conference paper
  • 463 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3153)

Abstract

This paper deals with the compositional verification of sequential programs. This consists in deciding whether or not a given set of local structural properties of the functions of a program implies a given global behavioural property of the program. Here we consider properties expressed in monadic second-order logic dealing with the control flow of the program and the function calls occuring during its execution. This problem has been investigated in relation with the security of open multi-application smart cards. We show that the compositionality is decidable for sequential programs whose control-flow graphs are of tree-width less than a fixed integer value, which includes in particular structured programs. Formally, we prove the decidability of MSO theories of families of hypergraphs obtained by uniform substitution of hyperedges by hypergraphs specified by MSO formulas.

Keywords

Compositional Verification Tree Automata Monadic Second-Order Logic 

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Grumberg, O., Long, D.: Model Checking and Modular Verification. ACM Trans. on Prog. Lang. & Syst. 16, 843–871 (1994)CrossRefGoogle Scholar
  2. 2.
    Abadi, M., Lamport, L.: Composing Specifications. ACM Transactions on Prog. Lang. and Systems (TOPLAS) 15, 73–132 (1993)CrossRefGoogle Scholar
  3. 3.
    M., C.E., Long, D.E., McMillan, K.L.: Compositional Model Checking. In: Proc. of the 4th Symp. on Logic in Comp. Sci (LICS 1989), pp. 353–362 (1989)Google Scholar
  4. 4.
    Jensen, T., Le Métayer, D., Thorn, T.: Verifying Security Properties of Control- Flow Graphs. In: Proc. of the 20th Symposium on Security and Privacy, Berkeley, pp. 89–103. IEEE Computer Society Press, Los Alamitos (1999)Google Scholar
  5. 5.
    Barthe, G., Gurov, D., Huisman, M.: Compositional Verification of Secure Applet Interactions. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 15–32. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  6. 6.
    Barthe, G., Courtieu, P., Dufay, G., Huisman, M., Mello de Sousa, S., Chugunov, G., Fredlund, L.A., Gurov, D.: Temporal Logic and Toolset for Applet Verification: Compositional Reasoning, Model Checking, Abstract Interpretation. Technical report, VERIFICARD Project, http://www.verificard.org/ (September 2002) Deliverable 4.1
  7. 7.
    Sprenger, C., Gurov, D., Huisman, M.: Simulation Logic, Applets and Compositional Verification. Technical Report 4890, INRIA (2003)Google Scholar
  8. 8.
    Dam, M., Gurov, D.: Compositional verification of CCS processes. In: Bjorner, D., Broy, M., Zamulin, A.V. (eds.) PSI 1999. LNCS, vol. 1755, pp. 247–256. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  9. 9.
    Stirling, C.: A complete compositional modal proof system for a subset of CCS. In: Brauer, W. (ed.) ICALP 1985. LNCS, vol. 194, pp. 475–486. Springer, Heidelberg (1985)CrossRefGoogle Scholar
  10. 10.
    Andersen, H.R., Stirling, C., Winskel, G.: A compositional proof system for the modal mu-calculus. In: 9th Symp. on Logic in Comp. Sci (LICS 1994), pp. 144–153. IEEE Comp. Soc. Press, Los Alamitos (1994)Google Scholar
  11. 11.
    Namjoshi, K.S., Trefler, R.J.: On the completeness of compositional reasoning. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 139–153. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  12. 12.
    Gurevich, Y.: Monadic Second-Order Theories. In: Barwise, J., Feferman, S. (eds.) Model Theoretic Logic, pp. 479–506. Springer, Heidelberg (1985)Google Scholar
  13. 13.
    Robertson, N., Seymour, P.: Some New Results on the Well-Quasi Ordering of Graphs. Annals of Discrete Math. 23, 343–354 (1984)MathSciNetGoogle Scholar
  14. 14.
    Thorup, M.: All structured programs have small tree-width and good register allocation. Inf. and Comp. 142, 159–181 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    Gustedt, J., Maehle, O., Telle, J.: The treewidth of java programs. In: Mount, D.M., Stein, C. (eds.) ALENEX 2002. LNCS, vol. 2409, p. 86. Springer, Heidelberg (2002) (to appear)CrossRefGoogle Scholar
  16. 16.
    Thomas, W.: Languages, automata, and logic. In: Rozenberg, Salomaa (eds.) Handbook of Formal Languages, vol. 3, pp. 389–455. Springer, Heidelberg (1997)Google Scholar
  17. 17.
    Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and secondorder logic. Theoretical Comp. Sci. 37, 51–75 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  18. 18.
    Courcelle, B.: The Monadic Second-order Logic of Graphs II: Infinite Graphs of Bounded Width. Math. Syst. Theory 21, 187–221 (1989)zbMATHCrossRefMathSciNetGoogle Scholar
  19. 19.
    Drewes, F., Kreowski, H.J., A., H.: Hyperedge Replacement Graph Grammars. In: Rozenberg, G. (ed.) Handbook of Graph Grammars and Computing by Graph Transformation, vol. 1, pp. 95–162. World Scientific, Singapore (1997)Google Scholar
  20. 20.
    Comon, H., Dauchet, M., Gilleron, R., Jacquemard, F., Lugiez, D., Tison, S., Tommasi, M.: Tree Automata Techniques and Applications. Technical report, LIFL – France (2003), http://www.grappa.univ-lille3.fr/tata/
  21. 21.
    Rabin, M.O.: Decidability of Second-Order Theories and Automata on Infinite Trees. Trans. of the A.M.S. 141, 1–35 (1969)zbMATHMathSciNetGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Olivier Ly
    • 1
  1. 1.LaBRIBordeaux I University 

Personalised recommendations