Abstract
This paper describes CVPP, a tool set for compositional verification of control–flow safety properties for programs with procedures. The compositional verification principle that underlies CVPP is based on maximal models constructed from component specifications. Maximal models replace the actual components when verifying the whole program, either for the purposes of modularity of verification or due to unavailability of the component implementations at verification time. A characteristic feature of the principle and the tool set is the distinction between program structure and behaviour. While behavioural properties are more abstract and convenient for specification purposes, structural ones are easier to manipulate, in particular when it comes to verification or the construction of maximal models. Therefore, CVPP also contains the means to characterise a given behavioural formula by a set of structural formulae. The paper presents the underlying framework for compositional verification and the components of the tool set. Several verification scenarios are described, as well as wrapper tools that support the automatic execution of such scenarios, providing appropriate pre– and post–processing to interface smoothly with the user and to encapsulate the inner workings of the tool set.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Arenas, M., Barcelo, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. In: Logic in Computer Science (LICS 2007), Washington, DC, USA, pp. 151–160. IEEE Computer Society, Los Alamitos (2007)
Alur, R., Chaudhuri, S.: Temporal reasoning for procedural programs. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 45–60. Springer, Heidelberg (2010)
Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467–481. Springer, Heidelberg (2004)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# Programming System: An Overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Boudol, G., Larsen, K.: Graphical versus logical specifications. Theoretical Computer Science 106, 3–20 (1992)
Chugunov, G., Fredlund, L.-Å., Gurov, D.: Model checking of multi-applet JavaCard applications. In: Smart Card Research and Advanced Application Conference (CARDIS 2002), pp. 87–95. USENIX Publications (2002)
Cleaveland, R., Parrow, J., Steffen, B.: A semantics based verification tool for finite state systems. In: International Symposium on Protocol Specification, Testing and Verification, pp. 287–302. North-Holland Publishing Co., Amsterdam (1990)
Das, M., Lerner, S., Seigle, M.: ESP: Path–sensitive program verification in polynomial time. In: Programming Language Design and Implementation (PLDI 2002), pp. 57–68. ACM, New York (2002)
Goldman, M., Katz, S.: MAVEN: Modular aspect verification. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 308–322. Springer, Heidelberg (2007)
Grumberg, O., Long, D.: Model checking and modular verification. ACM TOPLAS 16(3), 843–871 (1994)
Gurov, D., Huisman, M.: Interface abstraction for compositional verification. In: Software Engineering and Formal Methods (SEFM 2005), pp. 414–423 (2005)
Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 136–150. Springer, Heidelberg (2009)
Gurov, D., Huisman, M.: Reducing behavioural to structural properties of programs with procedures (2010); Full version, available upon request
Gurov, D., Huisman, M., Sprenger, C.: Compositional verification of sequential programs with procedures. Information and Computation 206(7), 840–868 (2008)
Huisman, M., Aktug, I., Gurov, D.: Program models for compositional verification. In: Liu, S., Araki, K. (eds.) ICFEM 2008. LNCS, vol. 5256, pp. 147–166. Springer, Heidelberg (2008)
Huisman, M., Gurov, D., Sprenger, C., Chugunov, G.: Checking absence of illicit applet interactions: A case study. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 84–98. Springer, Heidelberg (2004)
Kozen, D.: Results on the propositional μ-calculus. Theoretical Computer Science 27, 333–354 (1983)
Müller, P.: Modular Specification and Verification of Object-Oriented Programs. LNCS, vol. 2262. Springer, Heidelberg (2002)
Schneider, F.B.: Enforceable security policies. ACM Trans. Infinite Systems Security 3(1), 30–50 (2000)
Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universität München (2002)
Soleimanifard, S., Gurov, D., Huisman, M.: Procedure–modular verification of control flow safety properties. In: Workshop on Formal Techniques for Java Programs (FTfJP 2010) (2010)
Vallée-Rai, R., Hendren, L., Sundaresan, V., Lam, P., Gagnon, E., Co, P.: Soot - a Java Optimization Framework. In: CASCON 1999, pp. 125–135 (1999)
Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional mu-calculus. In: Logic in Computer Science (LICS 1995), pp. 14–24. IEEE, Los Alamitos (1995)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Huisman, M., Gurov, D. (2011). CVPP: A Tool Set for Compositional Verification of Control–Flow Safety Properties. In: Beckert, B., Marché, C. (eds) Formal Verification of Object-Oriented Software. FoVeOOS 2010. Lecture Notes in Computer Science, vol 6528. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-18070-5_8
Download citation
DOI: https://doi.org/10.1007/978-3-642-18070-5_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-18069-9
Online ISBN: 978-3-642-18070-5
eBook Packages: Computer ScienceComputer Science (R0)