| |
|
|
Electronic Systems Design Seminar
|
 |
|
Ensuring the correctness and reliability of a software system is a
challenging problem. Documenting correctness properties that the system should obey is straightforward. For example, it should not
dereference dangling pointers or read from unopened files. However, verifying that the system actually satisfies these properties is much
harder.
Automatic theorem proving provides a promising approach for verifying that a code fragment satisfies its correctness properties for all
possible input values. However, existing automatic theorem provers are unable to reason directly about code that uses iteration or recursion,
and instead require the programmer to help by supplying loop invariants and procedure specifications. The
burden of providing these annotations has so far limited the cost-effectiveness of such checking
tools.
This talk presents a novel, annotation-free approach to program checking. Our approach is based on an extended logic that provides
explicit support for iteration and recursion. Although the satisfiability of queries in this logic is undecidable in general, we
present an efficient semi-algorithm based on a combination of lazy abstraction, counter-example driven abstraction refinement,
and explicating, cooperating decision procedures for specific theories such as linear arithmetic.
The problem of deciding if a software system satisfies its correctness properties can be then expressed as a satisfiability query in this
logic, without burdening the programmer with supplying loop invariants and procedure specifications.
Cormac Flanagan is a research scientist at HP's Systems Research Center. His research has focused on the development of static checking tools that improve program reliability and reduce development cost by catching errors early in the development cycle. He has developed tools based on various combinations of program analysis, type systems, predicate abstraction, and theorem proving, and his primary motivation is the cost-effective application of these checking tools to large, real-world programs. He received his B.Sc. in computer science and mathematics from University College Dublin in 1990 and his Masters and Ph.D. in 1994 and 1997 from Rice University. For more information, see his homepage