Putting Static Analysis to Work for Verification: A Case Study

Tal Lev-Ami, Thomas Reps, Mooly Sagiv, and Reinhard Wilhelm

We study how program analysis can be used to:

Automatically prove partial correctness of correct programs.

Discover, locate, and diagnose bugs in incorrect programs.

Specifically, we present an algorithm that analyzes sorting programs that manipulate linked lists. A prototype of the algorithm has been implemented.

We show that the algorithm is sufficiently precise to discover that (correct versions) of bubble-sort and insertion-sort procedures do, in fact, produce correctly sorted lists as outputs, and that the invariant ``is-sorted'' is maintained by list-manipulation operations such as element-insertion, element-deletion, and even destructive list reversal and merging of two sorted lists. When we run the algorithm on erroneous versions of bubble-sort and insertion-sort procedures, it is able to discover and sometimes even locate and diagnose the error.

(Click here to access the paper: PostScript, PDF.)