Reasoning about Java Classes (Preliminary Report)

Bart Jacobs; Joachim van den Berg; Marieke Huisman; Martijn van Berkum; Ulrich Hensel; Hendrik Tews

doi:10.1145/286936.286973

Reasoning about Java Classes (Preliminary Report)

Bart Jacobs
, Joachim van den Berg
, Marieke Huisman
, Martijn van Berkum
, Ulrich Hensel
, Hendrik Tews

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

18 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	OOPSLA '98
Subtitle of host publication	Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 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

Keywords

n/a OA procedure

Access to Document

10.1145/286936.286973

ArticleAccepted author version, 262 KB

1 Article

Reasoning about Java Classes (Preliminary Report)
Jacobs, B., van den Berg, J., Huisman, M., van Berkum, M., Hensel, U. & Tews, H., Oct 1998, In: SIGPLAN Notices (ACM Special Interest Group on Programming Languages). 33, 10, p. 329-340 12 p.
Research output: Contribution to journal › Article › Academic › peer-review
57 Citations (Scopus)

Cite this

Jacobs, B., Berg, J. V. D., Huisman, M., van Berkum, M., Hensel, U., & Tews, H. (1998). Reasoning about Java Classes (Preliminary Report). In B. N. Freeman-Benson, & C. Chambers (Eds.), OOPSLA '98: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 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). OOPSLA '98: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 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.",

keywords = "n/a OA procedure",

author = "Bart Jacobs and Berg, \{Joachim van den\} and Marieke Huisman and \{van Berkum\}, Martijn and Ulrich Hensel and Hendrik Tews",

year = "1998",

doi = "10.1145/286936.286973",

language = "English",

pages = "329--340",

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

booktitle = "OOPSLA '98",

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, van Berkum, M, Hensel, U & Tews, H 1998, Reasoning about Java Classes (Preliminary Report). in BN Freeman-Benson & C Chambers (eds), OOPSLA '98: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 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.
OOPSLA '98: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 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 - van Berkum, Martijn

AU - Hensel, Ulrich

AU - Tews, Hendrik

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.

KW - n/a OA procedure

U2 - 10.1145/286936.286973

DO - 10.1145/286936.286973

M3 - Conference contribution

SP - 329

EP - 340

BT - OOPSLA '98

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, van Berkum M, Hensel U, Tews H. Reasoning about Java Classes (Preliminary Report). In Freeman-Benson BN, Chambers C, editors, OOPSLA '98: Proceedings of the 13th ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, 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

Keywords

Access to Document

Fingerprint

Research output

Reasoning about Java Classes (Preliminary Report)

Cite this