Automated theorem provers (ATPs) have long been a key component that software verification and analysis tools rely on. However, the basic interface provided by ATPs (validity/satisfiability checking of formulas) has not changed much in the last few decades. We argue that program analysis clients would benefit greatly if theorem provers were to provide a much richer interface. We describe our desiderata for such an interface to an ATP, the logics (theories) that an ATP for program analysis should support, and present how we have incorporated many of these ideas in Zap, an ATP built at Microsoft Research.
Thomas Ball leads the Testing, Verification and Measurement group in Microsoft Research. His research interests are in how combinations of program analysis, model checking and theorem proving techniques can help improve the correctness and reliability of programs. This is joint work with Shuvendu Lahiri and Madanlal Musuvathi.
Over the last 21 years, we've spent almost a person-millenium producing Cyc, an axiomatization of general human knowledge. Though still far from complete, Cyc contains over three million axioms. The need to express the range of things a person knows has led us to ever more expressive representation languages - currently we use an nth order predicate calculus with an overlay of contexts which are themselves first class objects. These pressures and others (e.g., elaboration tolerance) have driven us against numerous sorts of "scaling up" problems. In this talk I will briefly describe Cyc, the processes by which new axioms are added and deleted, applications of it, etc., but I will focus on some of these scaling up issues and approaches we have taken - and plan to take - to keep inference fast enough and to keep contradictions from being more than a nuisance.
Doug Lenat is one of the world's leading computer scientists, and is both the founder of the CYC® project and the president of Cycorp. He has been a Professor of Computer Science at Carnegie-Mellon University and Stanford University.
An overview is given of a number of recent developments in SAT and SAT Modulo Theories (SMT). In particular, based on our framework of Abstract DPLL and Abstract DPLL modulo Theories, we explain our DPLL(T) approach to SMT. Experimental results and future projects are discussed within the BarcelogicTools, a set of logic-based tools developed by our research group in Barcelona. At the 2005 SMT competition, BarcelogicTools won all four categories it participated in (out of the seven existing categories).
Roberto Nieuwenhuis is a full professor in the Software Department of the Technical University of Catalonia. His research interests are within the field of logic in computer science. This is joint work with Albert Oliveras.
In many verification applications the desired outcome is that the formula is unsatisfiable: A satisfying assignment essentially exhibits a bug and unsatisfiability implies a lack of bugs, at least for the property being verified. Most current high-performance satisfiability solvers and special-theory decision procedures are unable to provide proof of unsatisfiability. Since bugs have been discovered in many such programs long after being put into service, an uncheckable decision poses a significant problem if important economic or safety decisions are to be based upon it. This talk develops the thesis is that decision procedures can and should be designed with the ability to output an independently checkable proof. While finding a proof is hard, checking a proof can be straightforward if the proof system is simple enough. (By a "proof" we mean a real proof, with no steps omitted.) In practice, most underlying theories can produce a resolution proof. We argue that outputting such a proof does not place an undue burden on the decision procedures. We report on practical progress in this area for satisfiability solvers. Experiments have been carried out with what might be the first implementations of solver and proof checker that were developed completely independently, having only the specifications of the proof-file format as common knowledge. There is a trend toward combining high-performance satisfiability solvers with other theorem-proving methods. As the total systems become more complex, the need for "independent audits" becomes greater. Design goals for checkable proofs are proposed.
Allen Van Gelder is a Professor of Computer Science in the Jack Baskin School of Engineering at UCSC. His research interests include development of algorithms for propositional satisfiability, methods for verifiable software, theorem proving, analysis of algorithms, parallel algorithms, computer graphics, and scientific visualization.