Abstract
An important, challenging problem in the verification of imperative programs with shared, mutable state is the frame problem in the presence of data abstraction. That is, one must be able to specify and verify upper bounds on the set of memory locations a method can read and write without exposing that method's implementation.
Separation logic is now widely considered the most promising solution to this problem. However, unlike conventional verification approaches, separation logic assertions cannot mention heap-dependent expressions from the host programming language, such as method calls familiar to many developers. Moreover, separation logic-based verifiers are often based on symbolic execution. These symbolic execution-based verifiers typically do not support non-separating conjunction, and some of them rely on the developer to explicitly fold and unfold predicate definitions. Furthermore, several researchers have wondered whether it is possible to use verification condition generation and standard first-order provers instead of symbolic execution to automatically verify conformance with a separation logic specification.
In this article, we propose a variant of separation logic called implicit dynamic frames that supports heap-dependent expressions inside assertions. Conformance with an implicit dynamic frames specification can be checked by proving the validity of a number of first-order verification conditions. To show that these verification conditions can be discharged automatically by standard first-order provers, we have implemented our approach in a verifier prototype and have used this prototype to verify several challenging examples from related work. Our prototype automatically folds and unfolds predicate definitions, as required, during the proof and can reason about non-separating conjunction which is used in the specifications of some of these examples. Finally, we prove the soundness of the approach.
- Banerjee, A., Naumann, D., and Rosenberg, S. 2008. Regional logic for local reasoning about global invariants. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- Barnett, M., DeLine, R., Fähndrich, M., Leino, K. R. M., and Schulte, W. 2003. Verification of object-oriented programs with invariants. J. Obj. Technol. 3, 6.Google Scholar
- Barnett, M., Fahndrich, M., and Logozzo, F. 2010. Embedded contract languages. In Proceedings of the ACM Symposium on Applied Computing (SAC). Google ScholarDigital Library
- Barnett, M., Leino, K. R. M., and Schulte, W. 2004. The Spec# programming system: An overview. In Proceedings of the Workshop on Construction and Analysis of Safe, Secure, and Interoperable Smart devices (CASSIS). Google ScholarDigital Library
- Barnett, M. and Naumann, D. A. 2004. Friends need a bit more: Maintaining invariants over shared state. In Proceedings of the International Conference on Mathematics of Program Construction (MPC).Google Scholar
- Beckert, B., Hähnle, R., and Schmitt, P. H. 2007. Verification of Object-Oriented Software: The KeY Approach. Springer-Verlag. Google ScholarDigital Library
- Berdine, J., Calcagno, C., and O'Hearn, P. 2005. Symbolic execution with separation logic. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Google ScholarDigital Library
- Bornat, R. 2000. Proving pointer programs in hoare logic. In Proceedings of the International Conference on Mathematics of Program Construction (MPC). Google ScholarDigital Library
- Boyland, J. 2003. Checking interference with fractional permissions. In Proceedings of the International Symposium on Static Analysis. Google ScholarDigital Library
- Burdy, L., Cheon, Y., Cok, D., Ernst, M., Kiniry, J., Leavens, G. T., Leino, K. R. M., and Poll, E. 2005. An overview of JML tools and applications. Int. J. Softw. Tools Technol. Transfer 7, 3. Google ScholarDigital Library
- Calcagno, C., Distefano, D., OHearn, P., and Yang, H. 2009. Compositional shape analysis by means of BI-abduction. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Dahlweid, M., Moskal, M., Santen, T., Tobies, S., and Schulte, W. 2009. VCC: Contract-based modular verification of concurrent C. In Proceedings of the International Conference on Software Engineering (ICSE).Google Scholar
- Darvas, á. and Leino, K. R. M. 2007. Practical reasoning about invocations and implementations of pure methods. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE). Google ScholarDigital Library
- de Moura, L. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Google ScholarDigital Library
- Detlefs, D., Nelson, G., and Saxe, J. B. 2005. Simplify: A theorem prover for program checking. J. ACM 52, 3. Google ScholarDigital Library
- Dijkstra, E. W. 1975. Guarded commands, nondeterminacy and formal derivation of programs. Comm. ACM 18, 8. Google ScholarDigital Library
- Dinsdale-Young, T., Dodds, M., Gardner, P., Parkinson, M., and Vafeiadis, V. 2010. Concurrent abstract predicates. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- Distefano, D. and Parkinson, M. 2008. jStar: Towards practical verification for Java. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications (OOPSLA). Google ScholarDigital Library
- EIFFEL 2006. Eiffel: Analysis, design and programming language. Standard ECMA-367, ECMA International.Google Scholar
- Flanagan, C., Leino, K. R. M., Lillibridge, M., Nelson, G., Saxe, J. B., and Stata, R. 2002. Extended static checking for Java. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
- Gamma, E., Helm, R., Johnson, R., and Vlissides, J. 1994. Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley. Google ScholarDigital Library
- Haack, C. and Hurlin, C. 2009. Resource usage protocols for iterators. J. Obj. Technol. 8, 4.Google Scholar
- Hobor, A., Appel, A. W., and Nardelli, F. Z. 2008. Oracle semantics for concurrent separation logic. In Proceedings of the European Symposium on Programming (ESOP). Google ScholarDigital Library
- Jacobs, B. and Piessens, F. 2007. Inspector methods for state abstraction. J. Obj. Technol. 6, 5.Google Scholar
- Jacobs, B. and Piessens, F. 2011. Expressive modular fine-grained concurrency specification. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Jacobs, B., Piessens, F., Smans, J., and Leino, K. R. M. 2008. A programming model for concurrent object-oriented programs. ACM Trans. Program. Lang. Syst. 31, 1. Google ScholarDigital Library
- Jacobs, B., Smans, J., and Piessens, F. 2008. Verifying the composite pattern using separation logic. In Proceedings of the Specification and Verification of Component-Based Systems—Challenge Track (SAVCBS).Google Scholar
- Jacobs, B., Smans, J., and Piessens, F. 2010. A quick tour of the VeriFast program verifier. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Google ScholarDigital Library
- Kassios, Y. 2006. Dynamic frames: Support for framing, dependencies and sharing without restrictions. In Proceedings of the International Symposium on Formal Methods (FM). Google ScholarDigital Library
- Krishnaswami, N. R. 2006. Reasoning about iterators with separation logic. In Proceedings of the Specification and Verification of Component-Based Systems (SAVCBS). Google ScholarDigital Library
- Leavens, G. T. 2006. JMLŠs rich, inherited specifications for behavioral subtypes. In Proceedings of the International Conference on Formal Engineering Methods (ICFEM). Google ScholarDigital Library
- Leavens, G. T., Leino, K. R. M., and Müller, P. 2007. Specification and verification challenges for sequential object-oriented programs. Formal Aspects Comput. 19, 2. Google ScholarCross Ref
- Leino, K. R. M. 2010. Dafny: An automatic program verifier for functional correctness. In Proceedings of the International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). Google ScholarDigital Library
- Leino, K. R. M. and Middelkoop, R. 2009. Proving consistency of pure methods and model fields. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE). Google ScholarDigital Library
- Leino, K. R. M. and Monahan, R. 2009. Reasoning about comprehensions with first-order smt solvers. In Proceedings of the ACM Symposium on Applied Computing (SAC). Google ScholarDigital Library
- Leino, K. R. M. and Müller, P. 2004. Object invariants in dynamic contexts. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP).Google Scholar
- Leino, K. R. M. and Müller, P. 2009. A basis for verifying multithreaded programs. In Proceedings of the European Symposium on Programming (ESOP). Google ScholarDigital Library
- Leino, K. R. M., Müller, P., and Smans, J. 2010. A basis for verifying multithreaded programs. In Proceedings of the European Symposium on Programming (ESOP). Google ScholarDigital Library
- Leino, K. R. M. and Nelson, G. 2002. Data abstraction and information hiding. ACM Trans. Program. Lang. Sys. 24, 5. Google ScholarDigital Library
- Leino, K. R. M., Poetzsch-Heffter, A., and Zhou, Y. 2002. Using data groups to specify and check side effects. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
- Leino, K. R. M. and Schulte, W. 2007. Using history invariants to verify observers. In Proceedings of the European Symposium on Programming (ESOP). Google ScholarDigital Library
- Malecha, G. and Morrisett, G. 2010. Mechanized verification with sharing. In Proceedings of the International Colloquium on Theoretical Aspects of Computing (ICTAC). Google ScholarDigital Library
- Middelkoop, R., Huizing, C., Kuiper, R., and Luit, E. J. 2008. nvariants for non-hierarchical object structures. In Proceedings of the Brazilian Symposium on Formal Methods (SBMF). Google ScholarDigital Library
- Müller, P. 2001. Modular specification and verification of object-oriented programs. Ph.D. dissertation, FernUniversität Hagen.Google Scholar
- Müller, P. and Ruskiewicz, J. N. 2011. Using debuggers to understand failed verification attempts. In Proceedings of the International Symposium on Formal Methods (FM). Google ScholarDigital Library
- Nanevski, A., Morrisett, G., Shinnar, A., Govereau, P., and Birkedal, L. 2008. Ynot: Reasoning with the awkward squad. In Proceedings of the International Conference on Functional Programming (ICFP).Google Scholar
- Nanevski, A., Vafeiadis, V., and Berdine, J. 2010. Structuring the verification of heap-manipulating programs. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Nguyen, H. H., David, C., Qin, S., and Chin, W.-N. 2007. Automated verification of shape and size properties via separation logic. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Google ScholarDigital Library
- Nguyen, H. H., Kuncak, V., and Chin, W.-N. 2008. Runtime checking for separation logic. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Google ScholarDigital Library
- O'Hearn, P., Reynolds, J., and Yang, H. 2001. Local reasoning about programs that alter data structures. In Proceedings of the International Workshop on Computer Science Logic (CSL). Google ScholarDigital Library
- Owicki, S. and Gries, D. 1976. Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, 5. Google ScholarDigital Library
- Pariente, D. and Ledinot, E. 2010. Formal verification of industrial C code using Frama-C: A case study. In Proceedings of the International Conference on Formal Verification of Object-Oriented Software (FoVeOOS).Google Scholar
- Parkinson, M. 2005. Local reasoning for Java. Ph.D. thesis, University of Cambridge.Google Scholar
- Parkinson, M. 2007. Class invariants: The end of the road? In Proceedings of the International Workshop on Aliasing, Confinement and Ownership in Object-Oriented Programming (IWACO).Google Scholar
- Parkinson, M. and Bierman, G. 2005. Separation logic and abstraction. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Parkinson, M. and Bierman, G. 2008. Separation logic, abstraction and inheritance. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Parkinson, M. and Summers, A. 2011. The relationship between separation logic and implicit dynamic frames. In Proceedings of the European Symposium on Programming (ESOP). Google ScholarDigital Library
- Reynolds, J. 2002. Separation logic: A logic for shared mutable data structures. In Proceedings of the Symposium on Logic in Computer Science (LICS). Google ScholarDigital Library
- Rival, X. and Chang, B.-Y. E. 2011. Calling context abstraction with shapes. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Rosenberg, S., Banerjee, A., and Naumann, D. A. 2010. Local reasoning and dynamic framing for the composite pattern and its clients. In Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments. Google ScholarDigital Library
- Rudich, A., Darvas, á., and Müller, P. 2008. Checking well-formedness of pure-method specifications. In Proceedings of the International Symposium on Formal Methods (FM). Google ScholarDigital Library
- Schoeller, B. 2007. Making classes provable through contracts. Ph.D. ETH Zurich.Google Scholar
- Smans, J., Jacobs, B., and Piessens, F. 2009. Implicit dynamic frames: Combining dynamic frames and separation logic. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- Smans, J., Jacobs, B., and Piessens, F. 2010. Heap-dependent expressions in separation logic. In Proceedings of the International Conference on Formal Techniques for Distributed Systems (FMOODS/FORTE). Google ScholarDigital Library
- Smans, J., Jacobs, B., Piessens, F., and Schulte, W. 2008. An automatic verifier for Java-like programs based on dynamic frames. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE). Google ScholarDigital Library
- Summers, A. J. and Drossopoulou, S. 2010. Considerate reasoning and the composite design pattern. In Proceedings of the Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Google ScholarDigital Library
- Tuch, H., Klein, G., and Norrish, M. 2007. Types, bytes, and separation logic. In Proceedings of the Symposium on Principles of Programming Languages (POPL). Google ScholarDigital Library
- Tuerk, T. 2009. A formalization of Smallfoot in HOL. In Proceedings of the International Conference on Theorem Proving in Higher-Order Logics (TPHOLs). Google ScholarDigital Library
- Tuerk, T. 2010. Local reasoning about while-loops. In Proceedings of the International Conference on Verified Software: Theories, Tools and Experiments—Theory Workshop (VS-Theory).Google Scholar
- van Staden, S., Calcagno, C., and Meyer, B. 2010. Verifying executable object-oriented specifications with separation logic. In Proceedings of the European Conference on Object-Oriented Programming (ECOOP). Google ScholarDigital Library
- Villard, J., Lozes, é., and Calcagno, C. 2009. Proving copyless message passing. In Proceedings of the Asian Symposium on Programming Languages and Systems (APLAS). Google ScholarDigital Library
- Zee, K., Kuncak, V., and Rinard, M. C. 2008. Full functional verification of linked data structures. In Proceedings of the Conference on Programming Language Design and Implementation (PLDI). Google ScholarDigital Library
Index Terms
- Implicit dynamic frames
Recommendations
VST-Floyd: A Separation Logic Tool to Verify Correctness of C Programs
The Verified Software Toolchain builds foundational machine-checked proofs of the functional correctness of C programs. Its program logic, Verifiable C, is a shallowly embedded higher-order separation Hoare logic which is proved sound in Coq with ...
Tactics for Proving Separation Logic Assertion in Coq Proof Assistant
ICVISP 2019: Proceedings of the 3rd International Conference on Vision, Image and Signal ProcessingThe verification of the correctness of large programs, particularly operating systems is an unmanageable but important endeavor. we are interested in verifying C programs with formal methods, the logic is separation logic, a Hoare-style program logic. ...
Automatic verification of Java programs with dynamic frames
AbstractFraming in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs Leavens et al. (Formal Aspects Comput (FACS) 19:159–189, 2007). The dynamic frames approach is a promising solution ...
Comments