Invited Speakers
- Mark Stickel, SRI International
Building Theorem Provers
This talk discusses some of the challenges of building a usable theorem prover. These include the chasm between theory and code, conflicting requirements, feature interaction, and competitive performance. The talk draws on the speaker's experiences with devising extensions of resolution and building theorem provers that have been used as embedded reasoners in various systems. - Konstantin Korovin, The University of Manchester
Instantiation-Based Automated Reasoning - From Theory to Practice
Instantiation-based automated reasoning aims at utilising industrial-strength SAT and SMT technologies in the more general context of first-order logic. The basic idea behind instantiation-based reasoning is to combine smart generation of instances with satisfiability checking of ground formulae.
There are many challenges in this area. They range from theoretical issues such as completeness, integration of theories and decidable fragments, to efficient implementation including inference strategies, indexing and redundancy elimination. In this talk I will overview recent advances in instantiation-based reasoning and present a modular approach allowing one to use off-the-shelf SAT and SMT solvers for ground formulae as part of general first-order reasoning. - Martin Rinard, MIT Computer Science and Artificial Intelligence Laboratory
Integrated Reasoning and Proof Choice Point Selection in the Jahob System (Mechanisms for Program Survival)
In recent years researchers have developed a wide range of powerful automated reasoning systems. We have leveraged these systems to build Jahob, a program specification, analysis, and verification system. In contrast to many such systems, which use a monolithic reasoning approach, Jahob provides a general integrated reasoning framework, which enables multiple automated reasoning systems to work together to prove the desired program correctness properties.
We have used Jahob to prove the full functional correctness of a collection of linked data structure implementations. The automated reasoning systems are able to automatically perform the vast majority of the reasoning steps required for this verification. But there are some complex verification conditions that they fail to prove. We have therefore developed a proof language, integrated into the underlying imperative Java programming language, that developers can use to control key choice points in the proof search space. Once the developer has resolved these choice points, the automated reasoning systems are able to complete the verification. This approach appropriately leverages both the developer's insight into the high-level structure of the proof and the ability of the automated reasoning systems to perform the mechanical steps required to prove the verification conditions.
Building on Jahob's success with this challenging program verification problem, we contemplate the possibility of verifying the complete absence of fatal errors in large software systems. We envision combining simple techniques that analyze the vast majority of the program with heavyweight techniques that analyze those more sophisticated parts of the program that may require arbitrarily sophisticated reasoning. Modularity mechanisms such as abstract data types enable the sound division of the program for this purpose. The goal is not a completely correct program, but a program that can survive any remaining errors to continue to provide acceptable service.
