Bali Publications

Papers (with corresponding slides and theory sources)

Overview µJava: Embedding a Programming Language in a Theorem Prover, in the 1999 Proceedings of the International Summer School Marktoberdorf Java - formal fundiert, presented at the JavaDays '98/JIT'98, in German Java source language Hoare Logic for NanoJava: Auxiliary Variables, Side Effects and Virtual Methods revisited, presented at FME 2002 Hoare Logic for Java in Isabelle/HOL, in special issue of CPE. 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, presented at the ECOOP 2000 Workshop on Formal Techniques for Java Programs and the TPHOLs 2000 Poster Session Machine-checking the Java Specification: Proving Type-Safety, in the Springer LNCS Vol. 1523: Formal Syntax and Semantics of Java. Javalight is Type-Safe - Definitely, presented at POPL98

Java Virtual Machine & Bytecode Verifier

• Verified Bytecode Verifiers
, presented at FOSSACS 2001
• Verified Lightweight Bytecode Verification,
  presented at ECOOP 2000 Workshop on Formal Techniques for Java Programs. Slides
• Proving the Soundness of a Java Bytecode Verifier Specification in Isabelle/HOL,
  presented at TACAS'99
• Proving the Soundness of a Java Bytecode Verifier in Isabelle/HOL,
  presented at the OOPSLA'98 workshop 'Formal Underpinnings of Java'
• Formalizing the Java Virtual Machine in Isabelle/HOL, technical report

Other related papers

• Hoare Logic for Mutual Recursion and Local Variables,
  presented at FST & TCS '99, Springer LNCS 1738, 1999
  Slides

Other Slides

• Axiomatic Semantics for Java_light
• Designing a Java Formalization in HOL
• Operational Semantics of Java and Subject Reduction