Project Bali

Project Bali has been concerned with the formalization of various aspects of the programming language Java in the theorem prover Isabelle/HOL.

Project State

• For the Java source language, we have formalized the type system and the operational semantics and have proved type-safety. Furthermore, we have developed an axiomatic semantics.
• For the Bytecode level, we have formalized a part of the JVM and proved its type-safety. Furthermore, we have verified a bytecode verifier and lightweight bytecode verification.
  
• Further work has been done in the successor project VerifiCard.

Posters

• Project Overview Diagram
• What Is Type-Safety?
• Bali: A Formalization of Java
• BVM: A Formalization of the JVM

Publications (papers, slides, Isabelle sources)

Latest Isabelle Theories

• Java formalization
• µJava formalization
• JVM formalization: see paper

Project Members

• Gerwin Klein
• Tobias Nipkow
• David von Oheimb
• Norbert Schirmer
• Leonor Prensa Nieto

Bali was funded by the DFG. It is a descendant of The "Deduktion" Project in München.