Assertion-driven Development and Analyses

Sarfraz Khurshid
University of Texas at Austin
http://users.ece.utexas.edu/~khurshid

Abstract:

To increase reliability, developers have long used assertions---logical 
statements that are expected to be true---as lightweight specifications 
of crucial properties of code. ÊAssertions have predominantly served
two purposes: documentation and runtime checking. ÊWe envision a far
broader role of assertions where they are the cornerstone of a wide
range of analyses that synergistically promise to bring about an
unprecedented increase in reliability.

This talk describes our ongoing work on assertion-driven development
and analyses, where developers first assert designs and then write
code, static analyses check conformance of code to designs, testing
checks correctness of executable code, and runtime checking detects
erroneous executions, which error recovery repairs as desired. ÊOur
vision is to enable new analyses that uniformly apply across the whole
spectrum of software design, development, and maintenance---static
checking, testing, runtime checking, and error recovery all use the
same assertions that developers write just once. ÊConsequently,
writing assertions becomes much more attractive. ÊAs developers write
more assertions, they benefit not only from the new analyses but also
from leveraging a host of existing analyses that use specifications.