A Type-Theoretic Memory Model for Verification of Sequential Java Programs

Joachim van den Berg, Marieke Huisman, Bart Jacobs, Erik Poll

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

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 languageEnglish
Title of host publicationRecent Trends in Algebraic Development Techniques, 14th International Workshop, WADT '99, Château de Bonas, France, September 15-18, 1999, Selected Papers
EditorsDidier Bert, Christine Choppy, Peter D. Mosses
PublisherSpringer Singapore
Pages1-21
Number of pages21
DOIs
Publication statusPublished - 1999
Externally publishedYes
Event14th International Workshop on Recent Trends in Algebraic Development Techniques, WADT 1999 - Réaup-Lisse, France
Duration: 15 Sep 199918 Sep 1999
Conference number: 14

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume1827

Conference

Conference14th International Workshop on Recent Trends in Algebraic Development Techniques, WADT 1999
Abbreviated titleWADT 1999
CountryFrance
CityRéaup-Lisse
Period15/09/9918/09/99

Fingerprint Dive into the research topics of 'A Type-Theoretic Memory Model for Verification of Sequential Java Programs'. Together they form a unique fingerprint.

Cite this