Skip to Main content Skip to Navigation
Conference papers

Reasoning about Java Programs with Aliasing and Frame Conditions

Claude Marché 1 Christine Paulin-Mohring 1 
1 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : Several tools exist for reasoning about Java programs annotated with JML specifications. A main issue is to deal with possible aliasing between objects and to handle correctly the frame conditions limiting the part of memory that a method is allowed to modify. Tools designed for automatic use (like ESC/Java) are not complete and even not necessarily correct. On the other side, tools which offer a full modeling of the program require a heavy user interaction for discharging proof obligations. In this paper, we present the modeling of Java programs used in the Krakatoa tool, which generates proof obligations expressed in a logic language suitable for both automatic and interactive reasoning. Using the Simplify automatic theorem prover, we are able to establish automatically more properties than static analysis tools, with a method which is guaranteed to be sound, assuming only the correctness of our logical interpretation of programs and specifications.
Document type :
Conference papers
Complete list of metadata

https://hal.inria.fr/hal-03274993
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Wednesday, June 30, 2021 - 4:09:56 PM
Last modification on : Saturday, June 25, 2022 - 10:51:57 PM
Long-term archiving on: : Friday, October 1, 2021 - 6:54:41 PM

File

marche05tphols.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Claude Marché, Christine Paulin-Mohring. Reasoning about Java Programs with Aliasing and Frame Conditions. Theorem Proving in Higher Order Logics, 2005, Oxford, United Kingdom. pp.179-194, ⟨10.1007/11541868_12⟩. ⟨hal-03274993⟩

Share

Metrics

Record views

29

Files downloads

24