CW 355

Bart Jacobs, Frank Piessens
A $\pi$-Calculus Semantics of Java: The Full Definition

Abstract

We present a formal specification of the execution behavior of programs written in the Java programming language, by defining a mapping of Java programs to process expressions of the $\pi$-calculus. The specification is designed to support systems for the machine-aided verification of the correctness of Java programs.

report.pdf / mailto: B. Jacobs