The current version differs from the previous versions in significant ways. The changes are given in two parts. ===================== Part 1 ======================== An item preceded by * refers to the version of 4/19/09, ** refers to the version of 4/20/09, no * refers to the version of 4/12/09 Title: Changed to "Foundations of Automated Deduction for Formal Verification" Abstract: Rewritten slightly to summarize the contents of the survey. 1. Introduction: p.1: First paragraph is more succinct. p.2: Added references to early papers and surveys. Added an enumeration of the applications of deduction in verification 2. Background p.4: The notation for substitutions and assignments is standardized to \{x \mapsto a, y \mapsto b \} p.6: I was asked to explain why the cut rule is not derivable. The text there is still very terse. I'm hoping it is visually obvious that we can't eliminate A with rules that only introduce new connectives. Otherwise, I would have to go into an explanation of cut elimination to justify the admissibility of the cut rule. I'm happy to do this if advised. p.7: Added an explanation of open premises. p.7/8: Improved the presentation of the modal systems and corrected the accessibility condition for S5. p.8/9: Improved the presentation of invariants, inductive invariants, bounded model checking, and k-induction. p.9/10: The Alloy encoding of m-ary relations over n elements requires $n^m$ atoms --- one for each m-tuple. *p.10: Sec 2.2: Added an informal explanation of the universal quantifier. p.11: Using M[x\mapsto a] to represent updates. Defined a free variables operation. p.12/13: Added a description of McCune's Robbins' conjecture proof. p.13: The notation for quantification and lambda abstraction is now (\forall (x: T). A). Minor improvements to the completeness argument. p.13/14: Added a list of metatheorems about FOL. p.15: The references to Gentzen and Skolem still have strange years (1969 and 1967) associated with them. There's a bunch of these that I'll try to fix. Some of these are in bibtex files that I don't control, but I'll make sure these are fixed. p.16, 17: The introduction to Higher-Order Logic is entirely new. The section on "The verification problems" has been eliminated. *p.18: Fixed several typos in the presentation of ordered resolution as an inference system. **p.20: Clarified the progress from DPLL to the present. *p.22: Added a motivation for interpolation based on bounded model checking. The presentation of the interpolant construction example is very terse. Is this topic expendable? *p.25/26: Several typos have been corrected in the union-find inference system, and the interface operations have also been explained properly. *p.26: The congruence closure explanation is clearer. The explanation of simplex has also been improved with a reference and definitions of basis and non-basis variables. *p.27: Some minor improvements to the presentation of the Groebner basis method. p.28: Added references for Parrilo and definition for "positive semi-definite". Small corrections in the definition of the signed interpretation for bit-vectors. *p.28/29: Expanded the explanation of the Nelson-Oppen method for combination decision procedures. p.29: Skolemization is described here. Does it need a longer explanation? p.30: Unification is explained here. Removed mention of set-of-support and hyper-resolution p.31: Added a simplified explanation of superposition. This does not connect up to the first-order case. An intrepid reader could do it, but it will take another page. p.32: Contrary to one referees claim, executability is mentioned in the opening paragraph of Sec. 5.1. * Expanded a bit on the Boyer-Moore "waterfall". p.34/35, Sec 5.2: Small improvements to the explanation of tactical proof checking, but this might still be too terse. p.36: Added a reference to the Flyspeck project. p.36/37: The treatment of Coq has been expanded to include Barendregt's cube. Dependent product and sum types are still there, though I agree with the reviewer that it is more perspicuous to refer to these as function and product. The paragraph on Nuprl is still there, but it can be removed if that is still the advice. p.38/39: Added a paragraph emphasizing the versatility and applications of Isabelle. I still want to emphasize the logical frameworks aspect of Isabelle to underline the generic nature of its automated tools. p.39, Sec 5.6: The treatment of PVS looks quite superficial. I'm happy to drop it if it looks redundant. p.40, sec 5.7: This section is also mostly unchanged. I think Maude is an important system for prototyping logical tools, but I'm okay with dropping it if it looks irrelevant. *p.41: The conclusions have been softened a bit. References: Nearly three pages of new references have been added. I'm happy to add or subtract others. I know the Bjoerner/de Moura integration of SMT and superposition. The idea was originally proposed by Chris Lynch. I like this work but I'm worried that it might be difficult to explain. ===================== Part 2 ======================== The list of changes by page number in the final version (version of 6/14/09). 1. Simplified the title to "Automated Deduction for Verification". My colleagues found the earlier title a bit pompous. The title they would prefer is "Deductive Techniques for Verification based on Satisfiability, Automated Proof Search, and Interactive Proof Checking", but that's a bit long. 2. Added a few high-level definitions and overview to convey the editorial slant of the survey. I've also shortened the list that starts at the bottom of the page. 3. I've moved the background reading to the opening paragraph of the section. 4. Adjusted the definition of formal semantics. 5. Merged the truth tables in Fig 1 into a single table. 8. Added some pointers to modal provers. Added variants of SAT: AllSAT, MAXSAT, and unsat cores. 9. Added reference to Cook-Levin and separated out invariants into a separate paragraph. 12. Removed the definition of free variables. 14. Move the Herbrand theorem material here from the proof search section. 15/16. The treatment of first-order theories has been expanded. 22. I've named the different SAT solvers. 25. The interpolant construction table is more explicit. 29. Added material on Fourier's method, and more references. 30. Extended the explanation of the use of Grobner basis. I've had to eliminate the Parrilo reference since I don't want to say something inaccurate. 34. Hinted at how the simple superposition system is extended to first-order. 35. Moved Maude to the front of this section. 43. Some modest changes to the PVS subsection, and several changes to the "Looking ahead" section. References. I've probably added two more pages worth of references.