Reasoning about Java programs in higher order logic using PVS and Isabelle
In case you object to the disclosure of your thesis, you can contact firstname.lastname@example.org
[S.l. : s.n.]
IPA dissertation series ; 2001-03
Number of pages
X, 240 p.
Display more detailsDisplay less details
This thesis describes the first steps of a project aimed at formal verification of Java programs. The work presented here is part of a larger project called LOOP, for Logic of Object Oriented Programming. A semantics for Java is described in type theory and it is shown how this semantics forms the basis for program verification. The verifications are done with the use of interactive theorem provers,namely PVS and Isabelle. Both theorem provers are described in some detail, resulting in a comparison of the strong and weak points of both systems. A Hoare logic is discussed, which is especially tailored to reasoning about Java. The LOOP project resulted in the construction of the so-called LOOP compiler, which takes Java classes as input and returns PVS or Isabelle theories, capturing the semantics of the Java program, as output. This thesis also briefly describes a specification language for Java, called JML (Java modeling language). This language can be used to specify Java classes.Finally, two non-trivial case studies are described in this thesis, verifying properties of standard Java library classes. The first case study verifies a class invariant over class Vector, the second case study verifies the functional behaviour of the class AbstractCollection
This item appears in the following Collection(s)
- Academic publications 
- Dissertations 
- Electronic publications 
- Open Access publications 
Upload full text
Use your RU credentials (u/z-number and password) to log in with SURFconext to upload a file for processing by the repository team.