From: Rupak Majumdar <rupak@EECS.Berkeley.EDU> Message-Id: <200209051806.LAA10925@ic.EECS.Berkeley.EDU> Subject: [ESD-Seminar Time Change] Cormac Flanagan on Monday, Sept 9 4-5 Date: Thu, 5 Sep 2002 11:06:10 -0700 (PDT) Please note that Cormac Flanagan's talk on Monday, September 9 is at 4 pm in 540 Cory, and NOT 5pm. ESD Seminar (540 Cory, Monday September 9, 4pm - 5pm) Title: Program Checking = Logic + Lambda Abstract: 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.
This archive was generated by hypermail 2b30 : 11/04/02 PST