Reasoning about Java Classes (Preliminary Report)

Bart Jacobs, Joachim van den Berg, Marieke Huisman, Martijn van Berkum

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

52 Citations (Scopus)

Abstract

We present the first results of a project called LOOP, on formal methods for the object-oriented language Java. It aims at verification of program properties, with support of modern tools. We use our own front-end tool (which is still partly under construction) for translating Java classes into higher order logic, and a back-end theorem prover (namely PVS, developed at SRI) for reasoning. In several examples we demonstrate how non-trivial properties of Java programs and classes can be proven following this two-step approach.
Original languageEnglish
Title of host publicationProceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998
EditorsBjørn N. Freeman-Benson, Craig Chambers
PublisherACM SIGCOMM
Pages329-340
Number of pages12
DOIs
Publication statusPublished - 1998
Externally publishedYes
Event13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998 - Vancouver, Canada
Duration: 18 Oct 199822 Oct 1998
Conference number: 13

Conference

Conference13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998
Abbreviated titleOOPSLA 1998
CountryCanada
CityVancouver
Period18/10/9822/10/98

Fingerprint Dive into the research topics of 'Reasoning about Java Classes (Preliminary Report)'. Together they form a unique fingerprint.

Cite this