Automatic verification of Java programs with dynamic frames

作者：Smans Jan^*; Jacobs Bart; Piessens Frank; Schulte Wolfram

来源：Formal Aspects of Computing, 2010, 22(3-4): 423-457.

DOI：10.1007/s00165-010-0148-1

• Program verification
• Dynamic frames
• Frame problem
• Data abstraction

Framing 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 to this problem. However, the approach is formalized in the context of an idealized logical framework. In particular, it is not clear the solution is suitable for use within a program verifier for a Java-like language based on verification condition generation and automated, first-order theorem proving. In this paper, we demonstrate that the dynamic frames approach can be integrated into an automatic verifier based on verification condition generation and automated theorem proving. The approach has been proven sound and has been implemented in a verifier prototype. The prototype has been used to prove correctness of several programming patterns considered challenging in related work.

• 出版日期2010-5
• 单位Microsoft