Sound reasoning about unchecked exceptions

In most software development projects, it is not feasi-ble for developers to handle explicitly all possible unusual events which may occur during program execution, such as arithmetic overflow, highly unusual environment conditions, heap memory or call stack exhaustion, or asynchronous thread cancellation. Modern programming languages pro-vide unchecked exceptions to deal with these circumstances safely and with minimal programming overhead. However, reasoning about programs in the presence of unchecked ex-ceptions is difficult, especially in a multithreaded setting where the system should survive the failure of a subsystem. We propose a static verification approach for multi-threaded programs with unchecked exceptions. Our ap-proach is an extension of the Spec # verification method-ology for object-oriented programs. It verifies that ob-jects encapsulating shared resources are always ready to be disposed of, by allowing ownership transfers to other threads only through well-nested parallel execution opera-tions. Also, the approach prevents developers from relying on invariants that may have been broken by a failure. We believe the programming style enforced by our approach leads to better programs, even in the absence of formal ver-ification. The proposed approach enables developers using mainstream languages to gain some of the benefits of ap-proaches based on isolated sub-processes. We believe this is the first verification approach that soundly verifies common exception handling and locking patterns in the presence of unchecked exceptions.