Siavash Soleimanifard
Dilian Gurov
ABSTRACT
This paper describes a novel technique for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity of verification is achieved by relativizing the correctness of global properties on the local properties rather than on the implementations of methods, and is based on the construction of maximal models. Tool support is provided by means of ProMoVer, a tool that is essentially a wrapper around a previously developed tool set for compositional verification of control flow safety properties, where program data is abstracted away completely. We evaluate the technique on a small but realistic case study.
- Doclet overview. http://java.sun.com/j2se/1.3/docs/tooldocs/javadoc/overview.html.Google Scholar
- R. Alur, M. Arenas, P. Barcelo, K. Etessami, N. Immerman, and L. Libkin. First-order and temporal logics for nested words. In Logic in Computer Science (LICS '07), pages 151--160, Washington, DC, USA, 2007. IEEE Computer Society. Google ScholarDigital Library
- R. Alur and S. Chaudhuri. Temporal reasoning for procedural programs. In Verification, Model Checking, and Abstract Interpretation (VMCAI '10), volume 5944 of LNCS, pages 45--60. Springer, 2010. Google ScholarDigital Library
- R. Alur, K. Etessami, and P. Madhusudan. A temporal logic for nested calls and returns. In Tools and Algorithms for the Analysis and Construction of Software (TACAS '04), volume 2998 of LNCS, pages 467--481. Springer, 2004.Google ScholarCross Ref
- R. Cleaveland, J. Parrow, and B. Steffen. A semantics based verification tool for finite state systems. In International Symposium on Protocol Specification, Testing and Verification, pages 287--302. North-Holland Publishing Co., 1990. Google ScholarDigital Library
- C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended static checking for java. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI '02), pages 234--245, 2002. Google ScholarDigital Library
- M. Goldman and S. Katz. MAVEN: Modular aspect verification. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS '07), volume 4424 of LNCS, pages 308--322. Springer, 2007. Google ScholarDigital Library
- D. Gurov and M. Huisman. Reducing behavioural to structural properties of programs with procedures. In Verification, Model Checking, and Abstract Interpretation (VMCAI '09), volume 5403 of LNCS, pages 136--150. Springer, 2009. Google ScholarDigital Library
- D. Gurov, M. Huisman, and C. Sprenger. Compositional verification of sequential programs with procedures. Information and Computation, 206(7):840--868, 2008. Google ScholarDigital Library
- E. Hubbers and E. Poll. Transactions and non-atomic api methods in java card: specification ambiguity and strange implementation behaviours.Google Scholar
- S. Kiefer, S. Schwoon, and D. Suwimonteerabuth. Moped - a model-checker for pushdown systems. http://www.informatik.uni-stuttgart.de/fmi/szs/tools/moped/.Google Scholar
- D. Kozen. Results on the propositional μ-calculus. Theoretical Computer Science, 27:333--354, 1983.Google ScholarCross Ref
- G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. R. Cok, P. Müller, J. Kiniry, and P. Chalin. JML Reference Manual, Feb. 2007. Department of Computer Science, Iowa State University. Available from http://www.jmlspecs.org.Google Scholar
- P. Müller. Modular Specification and Verification of Object-Oriented Programs, volume 2262 of LNCS. Springer, 2002.Google Scholar
- S. Soleimanifard, D. Gurov, and M. Huisman. ProMoVer, a tool for procedure-modular verification: A tool web interface. http://www.csc.kth.se/~siavashs/ProMoVer/promover.php.Google Scholar
- C. Stirling. Modal and Temporal Logics of Processes. Springer, 2001. Google ScholarDigital Library
- R. Vallée-Rai, L. Hendren, V. Sundaresan, P. Lam, E. Gagnon, and P. Co. Soot - a Java Optimization Framework. In CASCON '99, pages 125--135, 1999.Google Scholar
Index Terms
- Procedure-modular verification of control flow safety properties
Recommendations
Procedure-modular specification and verification of temporal safety properties
This paper describes ProMoVer, a tool for fully automated procedure-modular verification of Java programs equipped with method-local and global assertions that specify safety properties of sequences of method invocations. Modularity at the procedure-...
An automata-theoretic approach to modular model checking
In modular verification the specification of a module consists of two part. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the system in which the module is interacting. This is called the ...
On the complexity of modular model checking
LICS '95: Proceedings of the 10th Annual IEEE Symposium on Logic in Computer ScienceIn modular verification the specification of a module consists of two parts. One part describes the guaranteed behavior of the module. The other part describes the assumed behavior of the environment with which the module is interacting. This is called ...
Comments