Semantics of Java-like Programming Languages
- Hoare Logic for NanoJava: Auxiliary Variables, Side Effects and Virtual Methods revisited.
Joint work with Tobias Nipkow,
presented at FME 2002
- Hoare Logic for Java in Isabelle/HOL
in special issue of CPE, 2001.
- Analyzing Java in Isabelle/HOL:
Formalization, Type Safety and Hoare Logic
Ph.D. thesis, Technische Universität München. Official Electronic Publication
- Axiomatic Semantics for Javalight in Isabelle/HOL
presented at the ECOOP 2000 Workshop on Formal Techniques for Java Programs
and the TPHOLs 2000 Poster Session
-
µJava: Embedding a Programming Language in a Theorem Prover.
Joint paper with Tobias Nipkow and Cornelia Pusch,
in the 1999 Proceedings of the International Summer School Marktoberdorf 1999.
-
Hoare Logic for Mutual Recursion and Local Variables.
Presented at FST&TCS '99, Springer LNCS 1738, 1999
-
Machine-checking the Java Specification: Proving Type-Safety
Joint work with Tobias Nipkow, a chapter of
Springer LNCS Vol. 1523: Formal Syntax and Semantics of Java, 1999
-
Java - formal fundiert
Joint paper with Cornelia Pusch, presented at
the JavaDays '98/JIT'98, in German
-
Javalight is Type-Safe - Definitely
Joint work with Tobias Nipkow, presented at
POPL98,
ACM Press SIGPLAN, 1998
|
|