Reasoning about Java Classes (Preliminary Report)

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

doi:10.1145/286936.286973

Reasoning about Java Classes (Preliminary Report)

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

57 Citations (Scopus)

9 Downloads (Pure)

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 language	English
Title of host publication	Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998
Editors	Bjørn N. Freeman-Benson, Craig Chambers
Publisher	ACM SIGCOMM
Pages	329-340
Number of pages	12
DOIs	https://doi.org/10.1145/286936.286973
Publication status	Published - 1998
Externally published	Yes
Event	13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998 - Vancouver, Canada Duration: 18 Oct 1998 → 22 Oct 1998 Conference number: 13

Conference

Conference	13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998
Abbreviated title	OOPSLA 1998
Country/Territory	Canada
City	Vancouver
Period	18/10/98 → 22/10/98

Access to Document

10.1145/286936.286973

Jacobs-1998-Reasoning-about-java-classesAccepted author version, 324 KB

Cite this

Jacobs, B., Berg, J. V. D., Huisman, M., & Berkum, M. V. (1998). Reasoning about Java Classes (Preliminary Report). In B. N. Freeman-Benson, & C. Chambers (Eds.), Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998 (pp. 329-340). ACM SIGCOMM. https://doi.org/10.1145/286936.286973

Jacobs, Bart ; Berg, Joachim van den ; Huisman, Marieke et al. / Reasoning about Java Classes (Preliminary Report). Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998. editor / Bjørn N. Freeman-Benson ; Craig Chambers. ACM SIGCOMM, 1998. pp. 329-340

@inproceedings{01352547bd0a418097d110d03b5e8205,

title = "Reasoning about Java Classes (Preliminary Report)",

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.",

author = "Bart Jacobs and Berg, {Joachim van den} and Marieke Huisman and Berkum, {Martijn van}",

year = "1998",

doi = "10.1145/286936.286973",

language = "English",

pages = "329--340",

editor = "Freeman-Benson, {Bj{\o}rn N.} and Craig Chambers",

booktitle = "Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998",

publisher = "ACM SIGCOMM",

note = "13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998, OOPSLA 1998 ; Conference date: 18-10-1998 Through 22-10-1998",

}

Jacobs, B, Berg, JVD, Huisman, M & Berkum, MV 1998, Reasoning about Java Classes (Preliminary Report). in BN Freeman-Benson & C Chambers (eds), Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998. ACM SIGCOMM, pp. 329-340, 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998, Vancouver, British Columbia, Canada, 18/10/98. https://doi.org/10.1145/286936.286973

Reasoning about Java Classes (Preliminary Report). / Jacobs, Bart; Berg, Joachim van den; Huisman, Marieke et al.
Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998. ed. / Bjørn N. Freeman-Benson; Craig Chambers. ACM SIGCOMM, 1998. p. 329-340.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Reasoning about Java Classes (Preliminary Report)

AU - Jacobs, Bart

AU - Berg, Joachim van den

AU - Huisman, Marieke

AU - Berkum, Martijn van

N1 - Conference code: 13

PY - 1998

Y1 - 1998

N2 - 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.

AB - 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.

U2 - 10.1145/286936.286973

DO - 10.1145/286936.286973

M3 - Conference contribution

SP - 329

EP - 340

BT - Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998

A2 - Freeman-Benson, Bjørn N.

A2 - Chambers, Craig

PB - ACM SIGCOMM

T2 - 13th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, OOPSLA 1998

Y2 - 18 October 1998 through 22 October 1998

ER -

Jacobs B, Berg JVD, Huisman M, Berkum MV. Reasoning about Java Classes (Preliminary Report). In Freeman-Benson BN, Chambers C, editors, Proceedings of the 1998 ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages Applications (OOPSLA '98), Vancouver, British Columbia, Canada, October 18-22, 1998. ACM SIGCOMM. 1998. p. 329-340 doi: 10.1145/286936.286973

Reasoning about Java Classes (Preliminary Report)

Abstract

Conference

Access to Document

Fingerprint

Cite this