Abstract
This paper explains the details of the memory model underlying the verification of sequential Java programs in the “LOOP” project ([14,20]). The building blocks of this memory are cells, which are untyped in the sense that they can store the contents of the fields of an arbitrary Java object. The main memory is modeled as three infinite series of such cells, one for storing instance variables on a heap, one for local variables and parameters on a stack, and and one for static (or class) variables. Verification on the basis of this memory model is illustrated both in PVS and in Isabelle/HOL, via several examples of Java programs, involving various subtleties of the language (wrt. memory storage).
Original language | English |
---|---|
Title of host publication | Recent Trends in Algebraic Development Techniques, 14th International Workshop, WADT '99, Château de Bonas, France, September 15-18, 1999, Selected Papers |
Editors | Didier Bert, Christine Choppy, Peter D. Mosses |
Publisher | Springer |
Pages | 1-21 |
Number of pages | 21 |
DOIs | |
Publication status | Published - 1999 |
Externally published | Yes |
Event | 14th International Workshop on Recent Trends in Algebraic Development Techniques, WADT 1999 - Réaup-Lisse, France Duration: 15 Sept 1999 → 18 Sept 1999 Conference number: 14 |
Publication series
Name | Lecture Notes in Computer Science |
---|---|
Publisher | Springer |
Volume | 1827 |
Conference
Conference | 14th International Workshop on Recent Trends in Algebraic Development Techniques, WADT 1999 |
---|---|
Abbreviated title | WADT 1999 |
Country/Territory | France |
City | Réaup-Lisse |
Period | 15/09/99 → 18/09/99 |