Inductive Proof Outlines for Exceptions in Multithreaded Java 1

In this paper we give an operational semantics and introduce an assertional proof system for exceptions in a multithreaded Java sublanguage.