Reasoning about Java Classes (Preliminary Report)

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

doi:10.1145/286942.286973

Reasoning about Java Classes (Preliminary Report)

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

^*Corresponding author for this work

Research output: Contribution to journal › Article › Academic › peer-review

57 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 language	English
Pages (from-to)	329-340
Number of pages	12
Journal	SIGPLAN Notices (ACM Special Interest Group on Programming Languages)
Volume	33
Issue number	10
DOIs	https://doi.org/10.1145/286942.286973
Publication status	Published - Oct 1998
Externally published	Yes

Keywords

n/a OA procedure

Access to Document

10.1145/286942.286973

Cite this

@article{78d58c5f2ed4454b85f2a406baa299ea,

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 {van den Berg}, Joachim and Marieke Huisman and {van Berkum}, Martijn and Ulrich Hensel and Hendrik Tews",

year = "1998",

month = oct,

doi = "10.1145/286942.286973",

language = "English",

volume = "33",

pages = "329--340",

journal = "SIGPLAN Notices (ACM Special Interest Group on Programming Languages)",

issn = "0362-1340",

publisher = "Association for Computing Machinery",

number = "10",

}

TY - JOUR

T1 - Reasoning about Java Classes (Preliminary Report)

AU - Jacobs, Bart

AU - van den Berg, Joachim

AU - Huisman, Marieke

AU - van Berkum, Martijn

AU - Hensel, Ulrich

AU - Tews, Hendrik

PY - 1998/10

Y1 - 1998/10

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

UR - http://www.scopus.com/inward/record.url?scp=0348137518&partnerID=8YFLogxK

U2 - 10.1145/286942.286973

DO - 10.1145/286942.286973

M3 - Article

AN - SCOPUS:0348137518

SN - 0362-1340

VL - 33

SP - 329

EP - 340

JO - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

JF - SIGPLAN Notices (ACM Special Interest Group on Programming Languages)

IS - 10

ER -

Reasoning about Java Classes (Preliminary Report)

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Reasoning about Java Classes (Preliminary Report)

Cite this