Sciweavers

FAC
2010

Automatic verification of Java programs with dynamic frames

13 years 29 days ago
Automatic verification of Java programs with dynamic frames
Framing in the presence of data abstraction is a challenging and important problem in the verification of object-oriented programs [LLM07]. 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.
Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Sc
Added 02 Mar 2011
Updated 02 Mar 2011
Type Journal
Year 2010
Where FAC
Authors Jan Smans, Bart Jacobs, Frank Piessens, Wolfram Schulte
Comments (0)