PRL Seminars

Creating correct programs is one of the grand goals of Computer Science. A new project tackling this problem is proposed: provide a system where developers can record in a machine-checkable form some of their knowledge of why their code is correct. The goal is to make it as easy as possible for a developer to include whatever correctness information s/he wishes to record, not to enforce complete correctness.

As a building block to be used towards this goal, extended assertions are proposed. Extended assertions are assertions relating the values of program expressions at different program points. For example, an extended assertion might say, "if a[x] is greater than 0 at entry to this function, then a[y] will be non-zero at exit". For sufficiently restricted forms of programs and assertions, these extended assertions can be translated into decidable validity checking problems and checked statically. A prototype system is demonstrated that translates extended assertions about suitably restricted C programs into formulas which can be checked by the CVC ("Cooperating Validity Checker") system.

CVC checks validity of quantifier-free first-order logical formulas with respect to a combination of background theories. CVC is a large (around 150Kloc of C++) and complex system. The talk concludes with a look at an alternative approach to implementing high-performance validity checkers like CVC.

Speaker

Aaron Stump is an assistant professor of Computer Science at Washington University in St. Louis. He completed a B.A. with a double major in Computer Science and Philosophy at Cornell University in 1997. He completed a Ph.D. in Computer Science at Stanford University in 2002, advised by Prof. David Dill. His research interests are in computational logic, automated reasoning, and formal verification.