| Home > Publications > Reports > Informatics (CW) |
CW 494
Bart Jacobs, Peter Müller, and Frank Piessens
Sound reasoning about unchecked exceptions: soundness proof
Abstract
In this note we formalize a multithreaded Java-like programming language with unchecked exceptions, try-catch blocks, and synchronized blocks, as well as method contracts, object invariants, block invariants, thread-local objects, and parallel execution statements. We further formalize our verification condition generation-based modular static verification approach that verifies that the program complies with its method contracts even in the presence of unchecked exceptions, and prove its soundness.
report.pdf (390K) / mailto: B. Jacobs