loading...
Sound reasoning about unchecked exceptions
London, England September 10-September 14
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2007.36Fifth IEEE International Conference o ...
 This Article 
 
PDF
HTML
 
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Bart Jacobs, Katholieke Universiteit Leuven
Peter Muller, Microsoft Research, Redmond
Frank Piessens, Katholieke Universiteit Leuven
In most software development projects, it is not feasible 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 provide unchecked exceptions to deal with these circumstances safely and with minimal programming overhead. However, reasoning about programs in the presence of unchecked exceptions is difficult, especially in a multithreaded setting where the system should survive the failure of a subsystem. We propose a static verification approach for multithreaded programs with unchecked exceptions. Our approach is an extension of the Spec# verification methodology for object-oriented programs. It verifies that objects encapsulating shared resources are always ready to be disposed of, by allowing ownership transfers to other threads only through well-nested parallel execution operations. 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 verification. The proposed approach enables developers using mainstream languages to gain some of the benefits of approaches 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.
Citation:
Bart Jacobs, Peter Muller, Frank Piessens, "Sound reasoning about unchecked exceptions," sefm, pp.113-122, Fifth IEEE International Conference on Software Engineering and Formal Methods (SEFM 2007), 2007
Usage of this product signifies your acceptance of the Terms of Use.