Assertion-based Verification: From Compile-time Checking to Runtime Error Recovery

University Of Texas At Austin, Austin TX

Investigators

Abstract

Proposal Number CCF-0702680 TITLE Assertion-based Verification: From Compile-time Checking to Runtime Error Recovery PI Sarfraz Khurshid Abstract This project investigates assertion-based repair---a novel methodology for enabling software systems to recover from errors before they manifest into failures. Traditional approaches to error recovery use assertion evaluations to detect erroneous states and specialized routines to repair them. Most of these routines are ad hoc, ill-understood, and unable to handle a variety of errors. The key insight of this project is to turn a violated assertion into a repair routine by using the assertion as a basis of performing repair. This project will develop systematic approaches that enable efficient repair using assertions written in common programming languages, such as Java. The repair approaches will be evaluated using a variety of complex data structures. Realization of the proposed methodology enables a unified framework for compile-time checking and runtime error recovery -- two software reliability methodologies that traditionally have deployed very different algorithms. The unification has the potential to significantly increase the quality of software. Any program that is annotated with assertions, which programmers already write comfortably, can be: (1) systematically checked before deployment using existing techniques; and (2) guaranteed to continue to execute without failure, once deployed, using the proposed methodology.