Automated deduction for verification

ABSTRACT

Automated deduction uses computation to perform symbolic logical reasoning. It has been a core technology for program verification from the very beginning. Satisfiability solvers for propositional and first-order logic significantly automate the task of deductive program verification. We introduce some of the basic deduction techniques used in software and hardware verification and outline the theoretical and engineering issues in building deductive verification tools. Beyond verification, deduction techniques can also be used to support a variety of applications including planning, program optimization, and program synthesis.

REFERENCES

• 1: Abdulla, P. A., Čer&abar;ns, K., Jonsson, B., and Tsay, Y.-K. 1996. General decidability theorems for infinite-state systems. In Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA, 313--321.
• 2: Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E., Eds. 1992a. Handbook of Logic in Computer Science; Volume 1 Background: Mathematical Structures. Oxford Science Publications, Oxford, UK.
• 3: Abramsky, S., Gabbay, D. M., and Maibaum, T. S. E., Eds. 1992b. Handbook of Logic in Computer Science; Volume 2 Background: Computational Structures. Oxford Science Publications, Oxford, UK.
• 4: Abrial, J.-R. 1980. The Specification Language Z: Syntax and Semantics. Programming Research Group, Oxford University, Oxford, UK.
• 5: Abrial, J.-R. 1996. The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge, MA.
• 6: Adams, A., Dunstan, M., Gottliebsen, H., Kelsey, T., Martin, U., and Owre, S. 2001. Computer algebra meets automated theorem proving: Integrating Maple and PVS. In Proceedings of the Theorem Proving in Higher Order Logics, TPHOLs 2001, R. J. Boulton and P. B. Jackson, Eds. Lecture Notes in Computer Science, vol. 2152. Springer-Verlag, Berlin, Germany, 27--42.
• 7: Amla, N., Du, X., Kuehlmann, A., Kurshan, R. P., and McMillan, K. L. 2005. An analysis of SAT-based model checking techniques in an industrial environment. In Prceedings of the Correct Hardware Design and Verification Methods: 13th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2005, D. Borrione and W. Paul, Eds. Lecture Notes in Computer Science, vol. 3725. Springer-Verlag, Berlin, Germany, 254--268.
• 8: Andrews, P. B. 1986. An Introduction to Logic and Type Theory: To Truth through Proof. Academic Press, New York, NY.
• 9: Andrews, P. B., Issar, S., Nesmith, D., and Pfenning, F. 1988. The TPS theorem proving system. In 9th International Conference on Automated Deduction (CADE), E. Lusk and R. Overbeek, Eds. Lecture Notes in Computer Science, vol. 310. Springer-Verlag, Berlin, Germany, 760--761.
• 10: Archer, M. and Heitmeyer, C. 1996. TAME: A specialized specification and verification system for timed automata. In Work In Progress (WIP) Proceedings of the 17th IEEE Real-Time Systems Symposium (RTSS'96), IEEE Computer Society Press, Los Alamitos, CA. (The WIP Proceedings is available at http://www.cs.bu.edu/pub/ieee-rts/rtss96/wip/proceedings.)
• 11: Audemard, G., Bertoli, P., Cimatti, A., Kornilowicz, A., and Sebastiani, R. 2002. A SAT based approach for solving formulas over Boolean and linear mathematical propositions. In CADE. Lecture Notes in Computer Science, vol. 2392. Springer-Verlag, Berlin, Germany, 195--210.
• 12: Baader, F. and Nipkow, T. 1998. Term Rewriting and All That. Cambridge University Press, Cambridge, MA.
• 13: Baader, F. and Snyder, W. 2001. Unification theory. Handbook of Automated Reasoning. Elsevier Science, Amsterdam, The Netherlands, 445--533.
• 14: Bachmair, L. and Ganzinger, H. 2001. Resolution theorem proving. Handbook of Automated Reasoning. Elsevier Science, Amsterdam, The Netherlands, 19--99.
• 15: Bachmair, L., Ganzinger, H., Lynch, C., and Snyder, W. 1992. Basic paramodulation and superposition. In CADE, D. Kapur, Ed. Lecture Notes in Computer Science, vol. 607. Springer-Verlag, Berlin, Germany, 462--476.
• 16: Bachmair, L., Tiwari, A., and Vigneron, L. 2003. Abstract congruence closure. J. Automat. Reason. 31, 2, 129--168.
• 17: Ball, T., Majumdar, R., Millstein, T., and Rajamani, S. 2001. Automatic predicate abstraction of C programs. In Proceedings of the SIGPLAN '01 Conference on Programming Language Design and Implementation, 2001. ACM, New York, 203--313.
• 18: Barendregt, H. P. 1992. Lambda calculi with types. In Handbook of Logic in Computer Science, vol. 2. Oxford University Press, Oxford, UK, Chapter 2, 117--309.
• 19: Barnett, M., DeLine, R., Fähndrich, M., Leino, K. R. M., Schulte, W., and Venter, H. 2005. The Spec# programming system: Challenges and directions. In Verified Software: Theories, Tools, Experiments, Proceedings of the 1st IFIP TC 2/WG 2.3 Conference. Lecture Notes in Computer Science, vol. 4171. Springer-Verlag, Berlin, Germany, 144--152.
• 20: Barrett, C., de Moura, L., and Stump, A. 2005. SMT-COMP: Satisfiability modulo theories competition. In Proceedings of the Symposium on Computer-Aided Verification, CAV '2005, Lecture Notes in Computer Science, vol. 3576. Springer-Verlag, Berlin, Germany, 20--23.
• 21: Barrett, C. and Tinelli, C. 2007. CVC3. In Proceedings of the 19th International Conference on Computer Aided Verification, CAV 2007. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 298--302.
• 22: Barrett, C., Tinelli, C., Sebastiani, R., and Seshia, S. 2009. Satisfiability modulo theories. See Biere et al. [2009].
• 23: Barrett, C. W., Dill, D. L., and Stump, A. 2002. Checking satisfiability of first-order formulas by incremental translation to SAT. In Proceedings of the Symposium on Computer-Aided Verification, CAV '02. Lecture Notes in Computer Science. Springer-Verlag, Berlin, Germany.
• 24: Barwise, J., Ed. 1978a. In Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 90. North-Holland, Amsterdam, Holland.
• 25: Barwise, J. 1978b. An introduction to first-order logic. In Handbook of Mathematical Logic. North-Holland, Amsterdam, The Netherlands, Chapter A1, 5--46.
• 26: Basu, S., Pollack, R., and Roy, M.-F. 2003. Algorithms in Real Algebraic Geometry. Springer-Verlag, Berlin, Germany.
• 27: Beckman, N., Nori, A. V., Rajamani, S. K., and Simmons, R. J. 2008. Proofs from tests. In Proceedings of the ACM/SIGSOFT International Symposium on Software Testing and Analysis, ISSTA 2008. ACM, New York, 3--14.
• 28: Belinfante, J. G. F. 1999. Computer proofs in Gödel's class theory with equational definitions for composite and cross. J. Autom. Reason. 22, 2, 311--339.
• 29: Bensalem, S., Lakhnech, Y., and Owre, S. 1998. InVeSt: A tool for the verification of invariants. In Proceedings of the International Conference on Computer-Aided Verification, CAV '98. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 505--510.
• 30: Berezin, S., Ganesh, V., and Dill, D. L. 2003. An online proof-producing decision procedure for mixed-integer linear arithmetic. In Proceedings of the 9th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2003. Lecture Notes in Computer Science, vol. 2619. Springer-Verlag, Berlin, Germany, 521--536.
• 31: Bertot, Y. and Castéran, P. 2004. Interactive Theorem Proving and Program Development. Springer. Coq home page: http://coq.inria.fr/.
• 32: Bevier, W. R., Hunt, Jr., W. A., Moore, J. S., and Young, W. D. 1989. An approach to systems verification. J. Automat. Reason. 5, 4 (Dec.), 411--428.
• 33: Biere, A. 2008. PicoSAT essentials. J. SAT 4, 2-4, 75--97.
• 34: Biere, A., Cimatti, A., Clarke, E., Fujita, M., and Zhu, Y. 1999. Symbolic model checking using SAT procedures instead of BDDs. In Proceedings of the ACM Design Automation Conference (DAC'99). ACM, New York.
• 35: Biere, A., Heule, M., van Maaren, H., and Walsh, T., Eds. 2009. Handbook of Satisfiability. IOS Press.
• 36: Blackburn, P., de Rijke, M., and Venema, Y. 2002. Modal Logic. Cambridge University Press, Cambridge, MA.
• 37: Bledsoe, W. W. and Bruell, P. 1974. A man-machine theorem-proving system. Artif. Intel. 5, 51--72.
• 38: Bockmayr, A. and Weispfenning, V. 2001. Solving numerical constraints. In Handbook of Automated Reasoning. Elsevier Science, Amsterdam, The Netherlands, 751--742.
• 39: Bofill, M., Nieuwenhuis, R., Oliveras, A., Rodríguez-Carbonell, E., and Rubio, A. 2008. The Barcelogic SMT solver. In Proceedings of the 20th International Conference on Computer Aided Verification, CAV 2008. Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 294--298.
• 40: Bogudlov, I., Lev-Ami, T., Reps, T. W., and Sagiv, M. 2007. Revamping TVLA: Making parametric shape analysis competitive. In Proceedings of the 19th International Conference on Computer-Aided Verification, CAV. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 221--225.
• 41: Boolos, G. S. and Jeffrey, R. C. 1989. Computability and Logic, third ed. Cambridge University Press, Cambridge, UK.
• 42: Börger, E., Grädel, E., and Gurevich, Y. 1997. The Classical Decision Problem. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, Germany.
• 43: Borovanský, P., Kirchner, C., Kirchner, H., and Moreau, P.-E. 2002. ELAN from a rewriting logic point of view. Theor. Comput. Sci. 285, 2, 155--185.
• 44: Boyer, R. S., Elspas, B., and Levitt, K. N. 1975. SELECT—A formal system for testing and debugging programs by symbolic execution. ACM SIGPLAN Notices 10, 6 (June), 234--245.
• 45: Boyer, R. S., Lusk, E. L., McCune, W., Overbeek, R. A., Stickel, M. E., and Wos, L. 1986. Set theory in first-order logic: Clauses for Gödel's axioms. J. Automat. Reason. 2, 3 (Sept.), 287--327.
• 46: Boyer, R. S. and Moore, J. S. 1975. Proving theorems about Lisp functions. J. ACM 22, 1 (Jan.), 129--144.
• 47: Boyer, R. S. and Moore, J. S. 1979. A Computational Logic. Academic Press, New York.
• 48: Boyer, R. S. and Moore, J. S. 1988. A Computational Logic Handbook. Academic Press, New York.
• 49: Bradley, A. R. and Manna, Z. 2007. The Calculus of Computation: Decision Procedures with Applications to Verification. Springer-Verlag, Berlin, Germany.
• 50: Bradley, A. R., Manna, Z., and Sipma, H. B. 2006. What's decidable about arrays? In Proceedings of the 7th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI. Lecture Notes in Computer Science, vol. 3855. Springer-Verlag, Berlin, Germany, 427--442.
• 51: Bruttomesso, R., Cimatti, A., Franzén, A., Griggio, A., and Sebastiani, R. 2008. The MathSAT 4 SMT solver. In Proceedings of the 20th International Conference on Computer Aided Verification, CAV 2008. Lecture Notes in Computer Science, vol. 5123. Springer-Verlag, Berlin, Germany, 299--303.
• 52: Bryant, R. 1992. Symbolic Boolean manipulation with ordered binary decision diagrams. ACM Comput. Surv. 24, 3 (Sept.), 293--318.
• 53: Bryant, R. E., Lahiri, S. K., and Seshia, S. A. 2002. Modeling and verifying systems using a logic of counter arithmetic with lambda expressions and uninterpreted functions. In Proceedings of the Symposium on Computer-Aided Verification, CAV '2002. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany.
• 54: Buchberger, B. 1976. A theoretical basis for the reduction of polynomials to canonical forms. ACM SIGSAM Bulletin 10, 3, 19--29.
• 55: Bultan, T., Gerber, R., and Pugh, W. 1997. Symbolic model checking of infinite state systems using Presburger arithmetic. In Proceedings of the International Conference on Computer-Aided Verification, CAV'97. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany, 400--411.
• 56: Bundy, A. 2001. The automation of proof by mathematical induction. In Handbook of Automated Reasoning, vol. I. Elsevier Science, Amsterdam, The Netherlands, Chapter 13, 845--911.
• 57: Burch, J. R., Clarke, E. M., McMillan, K. L., Dill, D. L., and Hwang, L. J. 1992. Symbolic model checking: 10²⁰ states and beyond. Inf. Comput. 98, 2 (June), 142--170.
• 58: Burris, S. N. and Sankappanavar, H. P. 1981. A course in universal algebra. Graduate Texts in Mathematics, vol. 78. Springer-Verlag, Berlin, Germany. (Revised edition online at http://thoralf.uwaterloo.ca/htdocs/ualg.html).
• 59: Carreño, V. and Muñoz, C. 2000. Formal analysis of parallel landing scenarios. In Proceedings of the 19th AIAA/IEEE Digital Avionics Systems Conference.
• 60: Church, A. 1936. An unsolvable problem of elementary number theory. Am. J. Math. 58, 345--363. (Reprinted in DAVIS [1965]).
• 61: Church, A. 1940. A formulation of the simple theory of types. J. Symb. Logic 5, 56--68.
• 62: Clarke, E. M., Grumberg, O., Jha, S., Lu, Y., and Veith, H. 2003. Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50, 5, 752--794.
• 63: Clarke, E. M., Grumberg, O., and Peled, D. 1999. Model Checking. MIT Press, Cambridge, MA.
• 64: Clarke, L. A. 1976. A system to generate test data and symbolically execute programs. IEEE Trans. Softw. Eng. 2, 3 (Sept.), 215--222.
• 65: Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., and Quesada, J. F. 1999. The Maude system. In Proceedings of the 10th International Conference on Rewriting Techniques and Applications (RTA-99). Lecture Notes in Computer Science, vol. 1631, Springer-Verlag, Berlin, Germany, 240--243.
• 66: Clavel, M., Durán, F., Eker, S., Meseguer, J., and Stehr, M.-O. 1999. Maude as a formal meta-tool. In Proceedings of the World Congress on Formal Methods (FM'99). Lecture Notes in Computer Science, vol. 1709. Springer-Verlag, Berlin, Germany, 1684--1703.
• 67: Cohen, P. J. 1969. Decision procedures for real and p-adic fields. Communi. Pure Appl. Math. 22, 2, 131--151.
• 68: Collins, G. 1975. Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages. Lecture Notes in Computer Science, vol. 33. Springer-Verlag, Berlin, Germany, 134--183.
• 69: Constable, R. L., Allen, S. F., Bromley, H. M., Cleaveland, W. R., Cremer, J. F., Harper, R. W., Howe, D. J., Knoblock, T. B., Mendler, N. P., Panangaden, P., Sasaki, J. T., and Smith, S. F. 1986. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ. Nuprl home page: http://www.cs.cornell.edu/Info/Projects/NuPRL/.
• 70: Cook, S. A. 1971. The complexity of theorem proving procedures. In Proceedings of the 3rd ACM Symposium on Theory of Computing. ACM, New York, 151--158.
• 71: Cooper, D. C. 1972. Theorem proving in arithmetic without multiplication. In Machine Intelligence 7. Edinburgh University Press, Edinburgh, UK, 91--99.
• 72: Coquand, T. and Huet, G. 1988. The calculus of constructions. Inf. Comput 76, 2/3, 95--120.
• 73: Corbett, J., Dwyer, M., Hatcliff, J., Pasareanu, C., Robby, Laubach, S., and Zheng, H. 2000. Bandera: Extracting finite-state models from Java source code. In Proceedings of the 22nd International Conference on Software Engineering. IEEE Computer Society Press, Los Alamitos, CA, 439--448.
• 74: Cotton, S. and Maler, O. 2006. Fast and flexible difference constraint propagation for DPLL(T). In SAT. Lecture Notes in Computer Science, vol. 4121. Springer-Verlag, Berlin, Germany, 170--183.
• 75: Cousot, P. and Cousot, R. 1977. Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM Symposium on Principles of Programming Languages. Association for Computing Machinery, Los Angeles, CA, 238--252.
• 76: Craig, W. 1957. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. Journal of Symbolic Logic 22, 3, 269--285.
• 77: D'Agostino, M., Gabbay, D. M., Hänle, R., and Posegga, J., Eds. 1999. Handbook of Tableau Methods. Kluwer Academic Publishers, Dordrecht.
• 78: Dalen, D. V. 1983. Logic and Structure. Springer-Verlag, Berlin, Germany.
• 79: Dantzig, G. and Curtis, B. 1973. Fourier-Motzkin elimination and its dual. J. Combinat. Theory 14, 288--297.
• 80: Darlington, J. 1981. An experimental program transformation and synthesis system. Artif. Intell. 16, 1, 1--46.
• 81: Davis, M., Ed. 1965. The Undecidable. Raven Press, Hewlett, NY.
• 82: Davis, M., Logemann, G., and Loveland, D. 1962. A machine program for theorem proving. Commun. ACM 5, 7 (July), 394--397. (Reprinted in Siekmann and Wrightson Siekmann and Wrightson [1983], pages 267--270, 1983.)
• 83: Davis, M. and Putnam, H. 1960. A computing procedure for quantification theory. J. ACM 7, 3, 201--215.
• 84: de Bruijn, N. G. 1970. The mathematical language AUTOMATH, its usage and some of its extensions. In Symposium on Automatic Demonstration. Lecture Notes in Mathematics, vol. 125. Springer-Verlag, Berlin, Germany, 29--61.
• 85: de Bruijn, N. G. 1980. A survey of the project Automath. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism. Academic Press, Orlando, FL, 589--606.
• 86: de Moura, L., Dutertre, B., and Shankar, N. 2007. A tutorial on satisfiability modulo theories. In Proceedings of the 19th International Conference on Computer Aided Verification, CAV 2007. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 20--36.
• 87: de Moura, L., Rueß, H., and Sorea, M. 2002. Lazy theorem proving for bounded model checking over infinite domains. In Proceedings of the 18th International Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 2392. Springer-Verlag, Berlin, Germany, 438--455.
• 88: de Moura, L. M. and Bjørner, N. 2008. Z3: An efficient SMT solver. In Proceedings of the 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2008. Lecture Notes in Computer Science, vol. 4963. Springer-Verlag, Berlin, Germany, 337--340.
• 89: Delzanno, G. and Podelski, A. 2001. Constraint-based deductive model checking. Softw. Tools Tech. Trans. 3, 3, 250--270.
• 90: Detlefs, D., Nelson, G., and Saxe, J. B. 2003. Simplify: A theorem prover for program checking. Tech. Rep. HPL-2003-148, HP Labs.
• 91: Detlefs, D. L., Leino, K. R. M., Nelson, G., and Saxe, J. B. 1998. Extended static checking. Tech. Rep. 159, COMPAQ Systems Research Center.
• 92: Dowek, G. 2001. Higher-order unification and matching. In Handbook of Automated Reasoning, vol. II. Elsevier Science, Amsterdam, The Netherlands, Chapter 16, 1009--1062.
• 93: Downey, P. J. and Sethi, R. 1978. Assignment commands with array references. J. ACM 25, 4, 652--666.
• 94: D'Silva, V., Kroening, D., and Weissenbacher, G. 2008. A survey of automated techniques for formal software verification. IEEE Trans. CAD of Integrated Circ. Syst. 27, 7, 1165--1178.
• 95: Dutertre, B. and de Moura, L. 2006a. A fast linear-arithmetic solver for DPLL(T). In Proceedings of the 18 International Conference on Computer-Aided Verification, CAV '2006. Lecture Notes in Computer Science, vol. 4144. Springer-Verlag, Berlin, Germany, 81--94.
• 96: Dutertre, B. and de Moura, L. 2006b. The Yices SMT solver. http://yices.csl.sri.com/.
• 97: Ebbinghaus, H.-D., Flum, J., and Thomas, W. 1984. Mathematical Logic. Undergraduate Texts in Mathematics. Springer-Verlag, Berlin, Germany.
• 98: Eén, N. and Sörensson, N. 2003. An extensible SAT-solver. In Proceedings of the 6th International Conference on Theory and Applications of Satisfiability Testing. Lecture Notes in Artificial Intelligence, Springer-Verlag, Berlin, Germany.
• 99: Eker, S., Laderoute, K., Lincoln, P., Sriram, M. G., and Talcott, C. L. 2003. Representing and simulating protein functional domains in signal transduction using maude. In Proceedings of the 1st International Workshop on Computational Methods in Systems Biology, CMSB 2003. Lecture Notes in Computer Science, vol. 2602. Springer-Verlag, Berlin, Germany, 164--165.
• 100: Elgaard, J., Klarlund, N., and Möller, A. 1998. Mona 1.x: New techniques for WS1S and WS2S. In Proceedings of the International Conference on Computer-Aided Verification, CAV '98. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany, 516--520.
• 101: Elkaduwe, D., Klein, G., and Elphinstone, K. 2008. Verified protection model of the seL4 microkernel. In Proceedings of the 2nd International Conference on Verified Software: Theories, Tools, Experiments, VSTTE 2008. Lecture Notes in Computer Science, vol. 5295. Springer-Verlag, Berlin, Germany, 99--114.
• 102: Elspas, B., Green, M., Moriconi, M., and Shostak, R. 1979. A JOVIAL verifier. Tech. rep., Computer Science Laboratory, SRI International. Jan.
• 103: Elspas, B., Levitt, K. N., Waldinger, R. J., and Waksman, A. 1972. An assessment of techniques for proving program correctness. ACM Comput. Surv. 4, 2, 97--147.
• 104: Emerson, E. A. 1990. Temporal and modal logic. In Handbook of Theoretical Computer Science. vol. B: Formal Models and Semantics. Elsevier and MIT Press, Amsterdam, The Netherlands, and Cambridge, MA, Chapter 16, 995--1072.
• 105: Enderton, H. B. 1972. A Mathematical Introduction to Logic. Academic Press, New York, NY.
• 106: Escobar, S., Meadows, C., and Meseguer, J. 2007. Equational cryptographic reasoning in the Maude-NRL protocol analyzer. Electr. Notes Theor. Comput. Sci. 171, 4, 23--36.
• 107: Feferman, S. 1978. Theories of finite type related to mathematical practice. In Handbook of Mathematical Logic. North-Holland, Amsterdam, The Netherlands, Chapter D4, 913--972.
• 108: Feferman, S. 2006. Tarski's influence on computer science. Logi. Meth. Comput. Sci. 2, 3:6, 1--13.
• 109: Filliâtre, J.-C. and Marché, C. 2007. The Why/Krakatoa/Caduceus platform for deductive program verification. In CAV. Lecture Notes in Computer Science, vol. 4590. Springer-Verlag, Berlin, Germany, 173--177.
• 110: Fischer, M. J. and Rabin, M. O. 1974. Super-exponential complexity of presburger arithmetic. In Complexity of Computation. American Mathematical Society, Providence, RI, 27--41.
• 111: Fitting, M. 1990. First-Order Logic and Automated Theorem Proving. Springer-Verlag, Berlin, Germany.
• 112: Flanagan, C., Joshi, R., Ou, X., and Saxe, J. B. 2003. Theorem proving using lazy proof explication. In Proceedings of the 15th International Conference on Computer-Aided Verification (CAV 2003). Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, Berlin, Germany, 355--367.
• 113: Floyd, R. W. 1967. Assigning meanings to programs. In Mathematical Aspects of Computer Science, American Mathematical Society. Providence, RI, 19--32.
• 114: Fourier, J. B. J. 1826. Solution d'une question particulière du calcul des inégalités. Nouveau Bulletin des Sciences par la Société philomathique de Paris, 99--100.
• 115: Frege, G. 1893--1903. Grundgesetze der Arithmetik, Begriffsschriftlich abgeleitet. Verlag Hermann Pohle, Jena.
• 116: Gabbay, D. M. and Guenthner, F., Eds. 1983. Handbook of Philosophical Logic--Volume I: Elements of Classical Logic. Synthese Library, vol. 164. D. Reidel Publishing Company, Dordrecht, Holland.
• 117: Gabbay, D. M. and Guenthner, F., Eds. 1984. Handbook of Philosophical Logic--Volume II: Extensions of Classical Logic. Synthese Library, vol. 165. D. Reidel Publishing Company, Dordrecht, Holland.
• 118: Gabbay, D. M. and Guenthner, F., Eds. 1985. Handbook of Philosophical Logic--Volume III: Alternatives to Classical Logic. Synthese Library, vol. 166. D. Reidel Publishing Company, Dordrecht, Holland.
• 119: Galler, B. A. and Fisher, M. J. 1964. An improved equivalence algorithm. Commun. ACM 7, 5, 301--303.
• 120: Ganzinger, H. and Korovin, K. 2006. Theory instantiation. In Proceedings of the 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR). Lecture Notes in Computer Science, vol. 4246. Springer-Verlag, Berlin, Germany, 497--511.
• 121: Gerhart, S. L., Musser, D. R., Thompson, D. H., Baker, D. A., Bates, R. L., Erickson, R. W., London, R. L., Taylor, D. G., and Wile, D. S. 1980. An overview of Affirm: A specification and verification system. In Information Processing '80, IFIP, North-Holland, Amsterdam, The Netherlands, 343--347.
• 122: Gilmore, P. C. 1960. A proof method for quantification theory: Its justification and realization. IBM J. Research Develop. 4, 28--35. (Reprinted in Siekmann and Wrightson Siekmann and Wrightson [1983], pages 151--161.)
• 123: Girard, J.-Y., Lafont, Y., and Taylor, P. 1989. Proofs and Types. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, Cambridge, MA.
• 124: Godefroid, P., Klarlund, N., and Sen, K. 2005. DART: Directed automated random testing. In Proceedings of the Conference on Programming Language Design and Implementation: PLDI. ACM, New York, 213--223.
• 125: Gödel, K. 1930. Über die vollständigkeit des logikkalküls. Ph.D. dissertation, University of Vienna. (Translated by Stefan Bauer-Mengelberg and reprinted in van Heijenoort [1967, pages 582--591].)
• 126: Gödel, K. 1967. On formally undecidable propositions of principia mathematica and related systems. (First published 1930 and 1931.)
• 127: Goguen, J., Kirchner, C., Megrelis, A., Meseguer, J., and Winkler, T. 1987. An introduction to OBJ3. In Proceedings of the 1st International Workshop on Conditional Term Rewriting Systems. Lecture Notes in Computer Science, vol. 308. Springer-Verlag, Berlin, Germany, 258--263.
• 128: Goldberg, E. and Novikov, Y. 2007. Berkmin: A fast and robust sat-solver. Disc. Appl. Math. 155, 12, 1549--1561.
• 129: Goldblatt, R. 1992. Logics of Time and Computation, second ed. CSLI. Lecture Notes, vol. 7. Center for the Study of Language and Information, Stanford, CA.
• 130: Gomes, C. P., Kautz, H., Sabharwal, A., and Selman, B. 2008. Satisfiability solvers. In Handbook of Knowledge Representation. Foundations of Artificial Intelligence, vol. 3. Elsevier, Amsterdam, The Netherlands, 89--134.
• 131: Gonthier, G. 2008. Formal proof: The four-color theorem. Notices Amer. Math. Soc. 55, 11 (Dec.), 1382--1394.
• 132: Goodstein, R. L. 1964. Recursive Number Theory. North-Holland, Amsterdam, The Netherlands.
• 133: Gordon, M. 1985. Why higher-order logic is a good formalism for specifying and verifying hardware. Tech. Rep. 77 University of Cambridge. Computer Laboratory, Cambridge UK. 153--177. (Reprinted in Yoeli [1990].)
• 134: Gordon, M. 1985. HOL: A machine oriented formulation of higher order logic. Tech. Rep. 68, University of Cambridge Computer Laboratory, Cambridge, England. July.
• 135: Gordon, M., Milner, R., Morris, L., Newey, M., and Wadsworth, C. 1977. A metalanguage for interactive proof in LCF. Tech. Rep. CSR-16-77, Department of Computer Science, University of Edinburgh, Edinburgh, UK.
• 136: Gordon, M., Milner, R., and Wadsworth, C. 1979. Edinburgh LCF: A Mechanized Logic of Computation. Lecture Notes in Computer Science, vol. 78. Springer-Verlag, Berlin, Germany.
• 137: Gordon, M. J. C. 1989. Mechanizing programming logics in higher-order logic. In Current Trends in Hardware Verification and Theorem Proving. Springer-Verlag, Berlin, Germany, 387--439.
• 138: Gordon, M. J. C. and Melham, T. F., Eds. 1993. Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic. Cambridge University Press, Cambridge, UK. HOL home page: http://www.cl.cam.ac.uk/Research/HVG/HOL/.
• 139: Greve, D., Wilding, M., and Van Fleet, W. 2003. A separation kernel formal security policy. In Proceedings of the 4th International Workshop on the ACL2 Theorem Prover. Boulder, CO. Available at http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/\#presentations%.
• 140: Gries, D. and Schneider, F. B. 1993. A Logical Approach to Discrete Math. Texts and Monographs in Computer Science. Springer-Verlag, Berlin, Germany.
• 141: Grumberg, O., Ed. 1997. Proceedings of the International Conference on Computer-Aided Verification, CAV'97. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany.
• 142: Gulwani, S. and Tiwari, A. 2006. Assertion checking over combined abstraction of linear arithmetic and uninterpreted functions. In Proceedings of the European Symposium on Programming, ESOP 2006. Lecture Notes in Computer Science, vol. 3924. Springer-Verlag, Berlin, Germany, 279--293.
• 143: Hales, T. C. 2002. A computer verification of the Kepler conjecture. In Proceedings of the International Congress of Mathematicians. Higher Education Press, Beijing, China, 795--804.
• 144: Hales, T. C. 2007. The Jordan curve theorem, formally and informally. AMM: The American Mathematical Monthly 114.
• 145: Hales, T. C., Harrison, J., McLaughlin, S., Nipkow, T., Obua, S., and Zumkeller, R. 2009. A revision of the proof of the Kepler conjecture. Disc. Comput. Geom. http://www.springerlink.com/content/552kw4u6330952jk/fulltext.pdf.
• 146: Halmos, P. R. 1960. Naive Set Theory. The University Series in Undergraduate Mathematics. Van Nostrand Reinhold Company, New York, NY.
• 147: Halpern, J. Y., Harper, R., Immerman, N., Kolaitis, P. G., Vardi, M., and Vianu, V. 2001. On the unusual effectiveness of logic in computer science. Bull. Symb. Logic 7, 2, 213--236.
• 148: Hamon, G., de Moura, L., and Rushby, J. 2004. Generating efficient test sets with a model checker. In Proceedings of the 2nd International Conference on Software Engineering and Formal Methods (SEFM). IEEE Computer Society, Press, Los Alamitos, CA, 261--270.
• 149: Hamon, G., de Moura, L., and Rushby, J. 2005. Automated test generation with SAL. Technical note, Computer Science Laboratory, SRI International, Menlo Park, CA. Sept. Available at: http://www.csl.sri.com/users/rushby/abstracts/sal-atg.
• 150: Hanna, F. K. and Daeche, N. 1986. Specification and verification of digital systems using higher-order predicate logic. IEE Proceedings 133 Part E, 5 (Sept.), 242--254.
• 151: Hantler, S. L. and King, J. C. 1976. An introduction to proving the correctness of programs. ACM Comput. Surv. 8, 3 (Sept.), 331--353.
• 152: Harper, R., Honsell, F., and Plotkin, G. D. 1987. A framework for defining logics. In Proceedings of the IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, Los Alamitos, CA.
• 153: Harrison, J. 1996. HOL Light: A tutorial introduction. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD '96), M. Srivas and A. Camilleri, Eds. Lecture Notes in Computer Science, vol. 1166. Springer-Verlag, Berlin, Germany, 265--269. HOL Light home page: http://www.cl.cam.ac.uk/~jrh13/hol-light/index.html.
• 154: Harrison, J. 2001. The LCF approach to theorem proving. Available from http://www.cl.cam.ac.uk/~jrh13/slides/manchester-12sep01/slides.pdf.
• 155: Harrison, J. 2006. Floating-point verification using theorem proving. In Formal Methods for Hardware Verification, 6th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM 2006. Lecture Notes in Computer Science, vol. 3965. Springer-Verlag, Berlin, Germany, 211--242.
• 156: Harrison, J. 2007. Verifying nonlinear real formulas via sums of squares. In Proceedings of the 20th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2007. Lecture Notes in Computer Science, vol. 4732. Springer-Verlag, Berlin, Germany, 102--118.
• 157: Harrison, J. 2009. Handbook of Practical Logic and Automated Reasoning. Cambridge University Press, Cambridge, MA.
• 158: Henkin, L. 1949. The completeness of first-order functional calculus. J. Symb. Logic 14, 3, 159--166.
• 159: Henkin, L. 1950. Completeness in the theory of types. J. Symb. Logic 15, 2 (June), 81--91.
• 160: Henkin, L. 1996. The discovery of my completeness proofs. BSL: Bull. Symb. Logic 2, 2, 127--158.
• 161: Henzinger, T. A., Jhala, R., Majumdar, R., and Sutre, G. 2003. Software verification with BLAST. In Proceedings of the 10th International Workshop on Model Checking of Software (SPIN). Lecture Notes in Computer Science, vol. 2648. Springer-Verlag, Berlin, Germany, 235--239. (BLAST home page: http://embedded.eecs.berkeley.edu/blast/.)
• 162: Herbrand, J. 1930. Recherches sur la théorie de la démonstration. Ph.D. dissertation, Université de Paris, Paris, France. (English translation published in van Heijenoort [1967] and Herbrand Herbrand [1971].)
• 163: Herbrand, J. 1971. Logical Writings. Harvard University Press.
• 164: Hierons, R. M., Bogdanov, K., Bowen, J. P., Cleaveland, R., Derrick, J., Dick, J., Gheorghe, M., Harman, M., Kapoor, K., Krause, P., Lüttgen, G., Simons, A. J. H., Vilkomir, S., Woodward, M. R., and Zedan, H. 2009. Using formal specifications to support testing. ACM Comput. Surv. 41, 2, 1--76.
• 165: Hilbert, D. 1902. Mathematical problems. Lecture delivered before the International Congress of Mathematicians at Paris in 1900. Bull. Amer. Math. Soc. 8, 437--479.
• 166: Hoare, C. A. R. 2003. The verifying compiler: A grand challenge for computing research. J. ACM 50, 1, 63--69.
• 167: Hoare, C. A. R. and Misra, J. 2008. Verified software: Theories, tools, experiments vision of a grand challenge project. In Verified Software: Theories, Tools, Experiments. Lecture Notes in Computer Science, vol. 4171. Springer-Verlag, Berlin, Germany.
• 168: Hodges, W. 1997. A Shorter Model Theory. Cambridge University Press, Cambridge, MA.
• 169: Hörmander, L. 1983. The Analysis of Linear Partial Differential Operators II: Differential Operators with Constant Coefficients. Grundlehren der math. Wissenschaften, vol. 257. Springer-Verlag, Berlin, Germany.
• 170: Howard, W. 1980. The formulas-as-types notion of construction. To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism. Academic Press, New York, 479--490.
• 171: Hu, A. J. and Vardi, M. Y., Eds. 1998. Proceedings of the International Conference Computer-Aided Verification, CAV '98. Lecture Notes in Computer Science, vol. 1427. Springer-Verlag, Berlin, Germany.
• 172: Hunt, Jr., W. A. 1989. Microprocessor design verification. J. Automat. Reason. 5, 4 (Dec.), 429--460.
• 173: Huth, M. R. A. and Ryan, M. D. 2000. Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, Cambridge, UK.
• 174: Jackson, D. 2006. Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge, UK.
• 175: Jackson, P. and Sheridan, D. 2004. Clause form conversions for Boolean circuits. In SAT (Selected Papers). Lecture Notes in Computer Science, vol. 3542. Springer-Verlag, Berlin, Germany, 183--198.
• 176: Jhala, R. and Majumdar, R. 2009. Software model checking. ACM Comput. Surv. 41, 4, Article 21 (September 2009), 57 pages. DOI 10.1145/1592434.1592438 http://doi.acm.org/10.1145/1592434.1592438.
• 177: Jones, C. B. 1990. Systematic Software Development Using VDM, second ed. Prentice-Hall International Series in Computer Science. Prentice-Hall, Hemel Hempstead, UK.
• 178: Jones, C. B. 1992. The search for tractable ways of reasoning about programs. Tech. Rep. UMCS-92-4-4, Department of Computer Science, University of Manchester, Manchester, UK. Mar.
• 179: Kaufmann, M., Manolios, P., and Moore, J. S. 2000. Computer-Aided Reasoning: An Approach. Advances in Formal Methods, vol. 3. Kluwer.
• 180: Kaufmann, M. and Moore, J. S. 1996. ACL2: An industrial strength version of NQTHM. In COMPASS '96 (Proceedings of the Eleventh Annual Conference on Computer Assurance). IEEE Washington Section, Gaithersburg, MD, 23--34.
• 181: Kautz, H. and Selman, B. 1996. Planning as satisfiability. In Proceedings of the 10th European Conference on Artificial Intelligence. Wiley, New York, 359--363.
• 182: Kemmerer, R. 1980. FDM—A specification and verification methodology. Tech. Rep. SP-4088, System Development Corporation.
• 183: Kesten, Y. and Pnueli, A. 1998. Modularization and abstraction: The keys to practical formal verification. In Proceedings of the Symposium on Mathematical Foundations of Computer Science. 54--71.
• 184: King, J. C. 1969. A program verifier. Ph.D. dissertation, Carnegie Mellon University, Pittsburgh, PA.
• 185: King, J. C. 1976. Symbolic execution and program testing. Comm. ACM 19, 7, 385--394.
• 186: King, J. C. and Floyd, R. W. 1970. An interpretation oriented theorem prover over integers. In STOC'70: Proceedings of the 2nd Annual ACM Symposium on Theory of Computing. ACM, New York, 169--179.
• 187: Kleene, S. C. 1952. Introduction to Metamathematics. North-Holland, Amsterdam, The Netherlands.
• 188: Kleene, S. C. 1967. Mathematical Logic. Wiley, New York.
• 189: Knapp, S. and Paul, W. 2007. Pervasive verification of distributed real-time systems. In Software System Reliability and Security. IOS Press, NATO Security Through Science Series. Sub-Series D: Information and Communication Security, vol. 9. 239--297.
• 190: Kozen, D. 1977. Complexity of finitely presented algebras. In Conference Record of the 9th Annual ACM Symposium on Theory of Computing. ACM, New York, 164--177.
• 191: Kroening, D., Clarke, E., and Yorav, K. 2003. Behavioral consistency of C and Verilog programs using bounded model checking. In Proceedings of DAC 2003. ACM, New York, 368--371.
• 192: Kröning, D. and Strichman, O. 2008. Decision Procedures: An Algorithmic Point of View. Springer-Verlag, Berlin, Germany.
• 193: Kunen, K. 1980. Set Theory: An Introduction to Independence Proofs. Studies in Logic and the Foundations of Mathematics, vol. 102. North-Holland, Amsterdam, The Netherlands.
• 194: Leivant, D. 1994. Higher order logic. In Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 2: Deduction Methodologies, Clarendon Press, Oxford, UK, 229--321.
• 195: Leroy, X. 2007. Formal verification of an optimizing compiler. In MEMOCODE. IEEE, Computer Society Press, Los Alamitos, CA, 25.
• 196: Levin, L. 1973. Universal search problems. Problemy Peredachi Informatsii 9, 3, 265--266. (English translation in Trakhtenbrot, B. A.: A survey of Russian approaches to Perebor (brute-force search) algorithms. Ann. Hist. Comput. 6 (1984), pages. 384--400.)
• 197: Liu, X., Kreitz, C., van Renesse, R., Hickey, J., Hayden, M., Birman, K. P., and Constable, R. L. 1999. Building reliable, high-performance communication systems from components. In Proceedings of the 17th Annual ACM Symposium on Operating Systems Principles (SOSP). ACM, New York, 80--92.
• 198: Luckham, D. C., German, S. M., von Henke, F. W., Karp, R. A., Milne, P. W., Oppen, D. C., Polak, W., and Scherlis, W. L. 1979. Stanford Pascal Verifier user manual. CSD Report STAN-CS-79-731, Stanford University, Stanford, CA. Mar.
• 199: Luo, Z. and Pollack, R. 1992. The LEGO proof development system: A user's manual. Tech. Rep. ECS-LFCS-92-211, University of Edinburgh, Edinburgh, UK.
• 200: Manna, Z., Stickel, M., and Waldinger, R. 1991. Monotonicity properties in automated deduction. In Artificial Intelligence and Mathematical Theorem of Computation: Papers in Honor of John McCarthy, Academic Press, Orlando, FL, 261--280.
• 201: Manna, Z. and Waldinger, R. A deductive approach to program synthesis. ACM Trans. Prog. Lang. Sys. 2, 1.
• 202: Manolios, P. and Vroon, D. 2007. Efficient circuit to CNF conversion. In Proceedings of the 10th International Conference in Theory and Applications of Satisfiability Testing—SAT 2007. Lecture Notes in Computer Science, vol. 4501. Springer. 4--9.
• 203: Marques-Silva, J. and Sakallah, K. 1999. GRASP: A search algorithm for propositional satisfiability. IEEE Trans. Comput. 48, 5 (May), 506--521.
• 204: Martin-Löf, P. 1980. Intuitionistic Type Theory. Bibliopolis, Napoli, Italy.
• 205: Matiyasevich, Y. V. 1993. Hilbert's Tenth Problem. MIT Press, Cambridge, MA.
• 206: McCarthy, J. 1962. Computer programs for checking mathematical proofs. In Recursive Function Theory, Proceedings of a Symposium in Pure Mathematics. vol. V. American Mathematical Society, Providence, RI, 219--227.
• 207: McCarthy, J. 1963. A basis for a mathematical theory of computation. In Computer Programming and Formal Systems, North-Holland, Amsterdam, The Netherlands.
• 208: McCune, W. 1997. Solution of the robbins problem. J. Automat. Reason. 19, 3 (Dec.), 263--276.
• 209: McCune, W. W. 1990. OTTER 2.0 users guide. Tech. Rep. ANL-90/9, Mathematics and Computer Science Division, Argonne National Laboratory, Argonne, IL. Mar.
• 210: McCune, W. W. 2007. The Prover9 reference manual. http://www.cs.wnm.edu/~mccune/prover9/manual-examples.html.
• 211: McMillan, K. L. 1993. Symbolic Model Checking. Kluwer Academic Publishers, Boston, MA.
• 212: McMillan, K. L. 2003. Interpolation and SAT-based model checking. In Proceedings of the 15th International Conference on Computer Aided Verification, CAV 2003. Lecture Notes in Computer Science, vol. 2725. Springer-Verlag, Berlin, Germany, 1--13.
• 213: Mendelson, E. 1964. Introduction to Mathematical Logic. The University Series in Undergraduate Mathematics. D. Van Nostrand Company, New York, NY.
• 214: Meseguer, J. 1989. General logics. In Proceedings of the Logic Colloquium '87. North Holland, Amsterdam, The Netherlands, 275--329.
• 215: Meseguer, J. and Rosu, G. 2005. Computational logical frameworks and generic program analysis technologies. In Proceedings of the 1st IFIP TC 2/WG 2.3 Verified Software: Theories, Tools, Experiments, VSTTE 2005. Lecture Notes in Computer Science, vol. 4171. Springer-Verlag, Berlin, Germany, 256--267.
• 216: Meyer, B. and Woodcock, J., Eds. 2008. In Proceedings of the 1st IFIP TC 2/WG 2.3 Verified Software: Theories, Tools, Experiments, VSTTE 2005. Lecture Notes in Computer Science, vol. 4171. Springer-Verlag, Berlin, Germany.
• 217: Millen, J. and Rueß, H. 2000. Protocol-independent secrecy. In Proceedings of the Symposium on Security and Privacy. IEEE Computer Society Press, Los Alamitos, CA, 110--119.
• 218: Miller, D. and Nadathur, G. 1986. Higher-order logic programming. In Proceedings of the IEEE Symposium on Logic Programming. IEEE Computer Society Press, Los Alamitos, CA.
• 219: Milner, R. 1972. Logic for computable functions: Description of a machine implementation. Tech. Rep. CS-TR-72-288, Stanford University, Stanford, CA.
• 220: Miner, P. S., Geser, A., Pike, L., and Maddalon, J. 2004. A unified fault-tolerance protocol. In Proceedings of the Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Y. Lakhnech and S. Yovine, Eds. Lecture Notes in Computer Science, vol. 3253. Springer-Verlag, Berlin, Germany, 167--182.
• 221: Mints, G. 1992. A Short Introduction to Modal Logic. CSLI Lecture Notes, vol. 30. Center for the Study of Language and Information, Stanford, CA.
• 222: Moskewicz, M. W., Madigan, C. F., Zhao, Y., Zhang, L., and Malik, S. 2001. Chaff: Engineering an efficient SAT solver. In Proceedings of the Design Automation Conference. ACM, New York, 530--535.
• 223: Nadathur, G. and Miller, D. 1990. Higher-order Horn clauses. J. ACM 37, 4, 777--814.
• 224: Nadathur, G. and Mitchell, D. J. 1999. System description: Teyjus—A compiler and abstract machine based implementation of λProlog. In Proceedings of the 16th Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, Berlin, Germany, 287--291.
• 225: Naur, P. 1966. Proof of algorithms by general snapshots. BIT 6, 310--316.
• 226: Nederpelt, R. P., Geuvers, J. H., and de Vrijer, R. C. 1994. Selected Papers on Automath. North-Holland, Amsterdam, The Netherlands.
• 227: Nelson, G. 1981. Techniques for program verification. Tech. Rep. CSL-81-10, Xerox Palo Alto Research Center, Palo Alto, CA.
• 228: Nelson, G. and Oppen, D. 1977. Fast decision algorithms based on congruence closure. Tech. Rep. STAN-CS-77-646, Computer Science Department, Stanford University, Stanford, CA.
• 229: Nelson, G. and Oppen, D. C. 1979. Simplification by cooperating decision procedures. ACM Trans. Program. Lang. Syst. 1, 2, 245--257.
• 230: Nieuwenhuis, R. and Oliveras, A. 2005. Proof-producing congruence closure. In Proceedings of the 16th International Conference on Term Rewriting and Applications, RTA'05. Lecture Notes in Computer Science, vol. 3467. Springer-Verlag, Berlin, Germany, 453--468.
• 231: Nieuwenhuis, R., Oliveras, A., and Tinelli, C. 2006. Solving SAT and SAT Modulo Theories: From an abstract Davis--Putnam--Logemann--Loveland procedure to DPLL(T). J. ACM 53, 6, 937--977.
• 232: Nieuwenhuis, R. and Rubio, A. 1992. Basic superposition is complete. In ESOP. Lecture Notes in Computer Science, vol. 582. Springer-Verlag, Berlin, Germany, 371--389.
• 233: Nieuwenhuis, R. and Rubio, A. 2001. Paramodulation-based theorem proving. In Handbook of Automated Reasoning. Elsevier Science, Amsterdam, The Netherlands, 371--443.
• 234: Nipkow, T., Paulson, L. C., and Wenzel, M. 2002. Isabelle/HOL: A Proof Assistant for Higher-Order Logic. Springer-Verlag, Berlin, Germany. (Isabelle home page: http://isabelle.in.tum.de/.)
• 235: O'Connor, R. 2005. Essential incompleteness of arithmetic verified by Coq. CoRR abs/cs/0505034. informal publication.
• 236: Ohlbach, H., Nonnengart, A., de Rijke, M., and Gabbay, D. 2001. Encoding two-valued nonclassical logics in classical logic. In Handbook of Automated Reasoning. Elsevier Science, Amsterdam, The Netherlands, 1403--1486.
• 237: Oppen, D. C. 1980. Complexity, convexity and combinations of theories. Theoret. Comput. Sci. 12, 291--302.
• 238: Owre, S., Rushby, J., Shankar, N., and von Henke, F. 1995. Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. Softw. Engineering 21, 2 (Feb.), 107--125. PVS home page: http://pvs.csl.sri.com.
• 239: Park, D. 1976. Finiteness is mu-ineffable. Theoret. Comput. Sci. 3, 173--181.
• 240: Parrilo, P. A. 2003. Semidefinite programming relaxations for semialgebraic problems. Math. Program 96, 2, 293--320.
• 241: Paulin-Mohring, C. 1993. Inductive definitions in the system Coq: Rules and properties. In Proceedings of the International Conference on Typed Lambda Calculi and Applications. Lecture Notes in Computer Science, vol. 664. Springer-Verlag, Berlin, Germany, 328--345.
• 242: Paulson, L. 1998. The inductive approach to verifying cryptographic protocols. J. Comput. Secur. 6, 1, 85--128.
• 243: Paulson, L. C. 1994. Isabelle: A Generic Theorem Prover. Lecture Notes in Computer Science, vol. 828. Springer-Verlag, Berlin, Germany. (Isabelle home page: http://www.cl.cam.ac.uk/research/hvg/Isabelle/.)
• 244: Paulson, L. C. 2003. The relative consistency of the axiom of choice mechanized using Isabelle/ZF. LMS J. Comput. Math. 6, 198--248.
• 245: Pfenning, F. 2001. Logical frameworks. In Handbook of Automated Reasoning, vol. II. Elsevier Science, Amsterdam, The Netherlands, Chapter 17, 1063--1147.
• 246: Pfenning, F. and Schürmann, C. 1999. Twelf—A meta-logical framework for deductive systems (system description). In Proceedings of the 16th International Conference on Automated Deduction (CADE-16). Lecture Notes in Artificial Intelligence, vol. 1632. Springer-Verlag, Berlin, Germany, 202--206.
• 247: Pnueli, A. and Shahar, E. 1996. A platform for combining deductive with algorithmic verification. In Proceedings of the 8th International Computer Aided Verification Conference. Lecture Notes in Computer Science, Springer-Verlag, Berlin, Germany. 184--195.
• 248: Prawitz, D. 1960. An improved proof procedure. Theoria 26, 102--139. (Reprinted in Siekmann and Wrightson [1983], pages 162--201, 1983.)
• 249: Pugh, W. 1992. A practical algorithm for exact array dependence analysis. Commun. ACM 35, 8, 102--114.
• 250: Quaife, A. 1992. Automated deduction in von Neumann-Bernays-Gödel set theory. J. Automat. Reason. 8, 1 (Feb.), 91--147.
• 251: Rabin, M. O. 1978. Decidable theories. In Handbook of Mathematical Logic. Studies in Logic and the Foundations of Mathematics, vol. 90. North-Holland, Amsterdam, The Netherlands, Chapter C8, 595--629.
• 252: Rajan, S., Shankar, N., and Srivas, M. 1995. An integration of model-checking with automated proof checking. In Proceedings of the Symposium on Computer-Aided Verification (CAV) 1995. Lecture Notes in Computer Science, vol. 939. Springer-Verlag, Berlin, Germany, 84--97.
• 253: Riazanov, A. and Voronkov, A. 2002. The design and implementation of VAMPIRE. AI Communications: Special issue on CASC 15, 2 (Sept.), 91--110.
• 254: Robinson, A. and Voronkov, A., Eds. 2001. Handbook of Automated Reasoning. Elsevier Science, Amsterdam, The Netherlands.
• 255: Robinson, J. A. 1965. A machine-oriented logic based on the resolution principle. J. ACM 12, 1, 23--41.
• 256: Robinson, L., Levitt, K. N., and Silverberg, B. A. 1979. The HDM Handbook. Computer Science Laboratory, SRI International, Menlo Park, CA. Three Volumes.
• 257: Rudnicki, P. 1992. An overview of the MIZAR project. In Proceedings of the 1992 Workshop on Types for Proofs and Programs. Båstad, Sweden, 311--330. (The complete proccedings are available at http://www.cs.chalmers.se/pub/cs-reports/baastad.92/; this particular paper is also available separately at http://web.cs.ualberta.ca/~piotr/Mizar/MizarOverview.ps.)
• 258: Ruess, H. and Shankar, N. 2004. Solving linear arithmetic constraints. Tech. Rep. CSL-SRI-04-01, SRI International, Computer Science Laboratory, 333 Ravenswood Ave, Menlo Park, CA, 94025. January. (Revised, August 2004.)
• 259: Rueß, H., Shankar, N., and Srivas, M. K. 1996. Modular verification of SRT division. In Proceedings of the Symposium on Computer-Aided Verification, CAV '96. Lecture Notes in Computer Science, vol. 1102. Springer-Verlag, Berlin, Germany, 123--134.
• 260: Russell, B. 1903. The Principles of Mathematics. Cambridge University Press, Cambridge, MA.
• 261: Russell, B. 1908. Mathematical logic based on the theory of types. Amer. J. Math. 30, 222--262.
• 262: Russinoff, D. M. 1988. A mechanical proof of quadratic reciprocity. J. Automat. Reason. 8, 1, 3--21.
• 263: Russinoff, D. M. 1999. A mechanically checked proof of correctness of the AMD K5 floating point square root microcode. Form. Meth. Syst. Des. 14, 1 (Jan.), 75--125.
• 264: Ryan, L. 2004. Efficient algorithms for clause-learning SAT solvers. M.S. thesis, Simon Fraser University.
• 265: Saaltink, M. 1997. The Z/EVES system. In ZUM '97: The Z Formal Specification Notation; 10th International Conference of Z Users. Lecture Notes in Computer Science, vol. 1212. Springer-Verlag, Berlin, Germany, 72--85.
• 266: Saïdi, H. and Graf, S. 1997. Construction of abstract state graphs with PVS. In Proceedings of the International Conference on Computer-Aided Verification, CAV'97. Lecture Notes in Computer Science, vol. 1254. Springer-Verlag, Berlin, Germany, 72--83.
• 267: Saïdi, H. and Shankar, N. 1999. Abstract and model check while you prove. In Proceedings of the International Conference on Computer-Aided Verification, CAV '99. Lecture Notes in Computer Science, vol. 1633. Springer-Verlag, Berlin, Germany, 443--454.
• 268: Schulz, S. 2002. E—A brainiac theorem prover. J. AI Communi. 15, 2/3, 111--126.
• 269: Scott, D. S. 1993. A type-theoretical alternative to ISWIM, CUCH, OWHY. Theoret. Comput. Sci. 121, 1&2, 411--440. (Typed notes circulated in 1969.)
• 270: Shankar, N. 1994. Metamathematics, Machines, and Gödel's Proof. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge, UK.
• 271: Shankar, N. 2005. Inference systems for logical algorithms. In FSTTCS 2005: Proceedings of the Symposium on Foundations of Software Technology and Theoretical Computer Science. Lecture Notes in Computer Science, vol. 3821. Springer-Verlag, Berlin, Germany, 60--78.
• 272: Shankar, N. and Rueß, H. 2002. Combining Shostak theories. In International Conference on Rewriting Techniques and Applications (RTA '02). Lecture Notes in Computer Science, vol. 2378. Springer-Verlag, Berlin, Germany, 1--18.
• 273: Sheeran, M., Singh, S., and Stålmarck, G. 2000. Checking safety properties using induction and a SAT-solver. In Proceedings of the Formal Methods in Computer-Aided Design (FMCAD 2000). Lecture Notes in Computer Science, vol. 1954. Springer-Verlag, Berlin, Germany, 108--125.
• 274: Shoenfield, J. R. 1967. Mathematical Logic. Addison-Wesley, Reading, MA.
• 275: Shostak, R. E. 1978. An algorithm for reasoning about equality. Commun. ACM 21, 7 (July), 583--585.
• 276: Shostak, R. E. 1984. Deciding combinations of theories. J. ACM 31, 1 (Jan.), 1--12.
• 277: Shostak, R. E., Schwartz, R., and Melliar-Smith, P. M. 1982. STP: A mechanized logic for specification and verification. In Proceedings of the 6th International Conference on Automated Deduction (CADE). Lecture Notes in Computer Science, vol. 138. Springer-Verlag, Berlin, Germany.
• 278: Siekmann, J. and Wrightson, G., Eds. 1983. Automation of Reasoning: Classical Papers on Computational Logic, Volumes 1 & 2. Springer-Verlag, Berlin, Germany.
• 279: Simon, L., Berre, D. L., and Hirsch, E. A. 2005. The SAT2002 competition. Ann. Math. Artif. Intell 43, 1, 307--342.
• 280: Skolem, T. 1967. The foundations of elementary arithmetic established by means of the recursive mode of thought, without the use of apparent variables ranging over infinite domains. In From Frege to Gödel: A Sourcebook of Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA, 302--333. (First published 1923.)
• 281: Skolem, T. A. 1962. Abstract Set Theory. Number 8 in Notre Dame Mathematical Lectures. University of Notre Dame Press, Notre Dame, IN.
• 282: Slind, K. and Norrish, M. 2008. A brief overview of HOL4. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2008. Lecture Notes in Computer Science, vol. 5170. Springer-Verlag, Berlin, Germany, 28--32.
• 283: Smith, D. R. 1990. KIDS: A semiautomatic program development system. IEEE Transactions on Software Engineering 16, 9 (September), 1024--1043.
• 284: Smith, M. K., Good, D. I., and Di Vito, B. L. 1988. Using the Gypsy methodology. Tech. Rep. 1, Computational Logic Inc. Jan.
• 285: Smullyan, R. M. 1968. First-Order Logic. Springer-Verlag, Berlin, Germany. (Republished by Courier Dover Publications, 1995.)
• 286: Spivey, J. M., Ed. 1993. The Z Notation: A Reference Manual, second ed. Prentice-Hall International Series in Computer Science. Prentice-Hall, Hemel Hempstead, UK.
• 287: Steele Jr., G. L. 1990. Common Lisp: The Language, second ed. Digital Press, Bedford, MA.
• 288: Stickel, M. E. 1985. Automated deduction by theory resolution. J. Automat. Reason. 1, 4 (Dec.), 333--355.
• 289: Stickel, M. E., Waldinger, R. J., and Chaudhri, V. K. 2000. A guide to SNARK. Tech. Note, SRI International Artificial Intelligence Center.
• 290: Stump, A., Barrett, C. W., and Dill, D. L. 2002. CVC: A cooperating validity checker. In Proceedings of the International Conference on Computer-Aided Verification, CAV'02. Lecture Notes in Computer Science, vol. 2404. Springer-Verlag, Berlin, Germany.
• 291: Stump, A., Barrett, C. W., Dill, D. L., and Levitt, J. R. 2001. A decision procedure for an extensional theory of arrays. In LICS. 29--37.
• 292: Suppes, P. 1972. Axiomatic Set Theory. Dover Publications, Inc., New York, NY.
• 293: Sutcliffe, G. and Suttner, C. B. 2006. The state of CASC. AI Commun. 19, 1, 35--48.
• 294: Szabo, M. E., Ed. 1969. The Collected Papers of Gerhard Gentzen. North-Holland, Amsterdam, The Netherlands.
• 295: Tarjan, R. E. 1975. Efficiency of a good but not linear set union algorithm. J. ACM 22, 2, 215--225.
• 296: Tarski, A. 1948. A Decision Method for Elementary Algebra and Geometry. University of California Press.
• 297: Tarski, A., Mostowski, A., and Robinson, R. M. 1971. Undecidable Theories. North-Holland, Amsterdam, The Netherlands.
• 298: The Coq Development Team. 2009. The Coq proof assistant reference manual version 8.2. Tech. rep., INRIA. Feb.
• 299: Théry, L. 1998. A certified version of Buchberger's algorithm. In Proceedings of 15th International Conference on Automated Deduction (CADE). Lecture Notes in Artificial Intelligence, vol. 1421. Springer-Verlag, Berlin, Germany, 349--364.
• 300: Tiwari, A. 2005. An algebraic approach for the unsatisfiability of nonlinear constraints. In Proceedings of the 14th Annual Conference on Computer Science Logic, CSL 2005. Lecture Notes in Computer Science, vol. 3634. Springer-Verlag, Berlin, Germany, 248--262.
• 301: Torlak, E. and Jackson, D. 2007. Kodkod: A relational model finder. In Proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2007. Lecture Notes in Computer Science, vol. 4424. Springer-Verlag, Berlin, Germany, 632--647.
• 302: Troelstra, A. and van Dalen, D. 1988. Constructivity in Mathematics. North-Holland, Amsterdam, The Netherlands.
• 303: Tseitin, G. 1968. On the complexity of derivation in propositional calculus. In Studies in Constructive Mathematics and Mathematical Logic, Part 11. Otdel, Leningrad, Russia, 115--125. (Reprinted in Siekmann and Wrightson [1983].)
• 304: Turing, A. M. 1965. On computable numbers, with an application to the Entscheidungsproblem. In The Undecidable. Raven Press, Hewlett, NY, 116--154. First published 1937.
• 305: van Benthem, J. and Doets, K. 1983. Higher-order logic. In Handbook of Philosophical Logic, Volume I: Elements of Classical Logic, Synthese Library, vol. 164. D. Reidel Publishing Co., Dordrecht, Chapter I.4, 275--329.
• 306: van den Berg, J. and Jacobs, B. 2001. The loop compiler for Java and JML. In Proceedings of the 7th International Conference on Tools and Algorithms for the Construction and Analysis of Systems: TACAS 2001, T. Margaria and W. Yi, Eds. Lecture Notes in Computer Science, vol. 2031. Springer-Verlag, Berlin, Germany, 299--312.
• 307: van Heijenoort, J., Ed. 1967. From Frege to Gödel: A Sourcebook of Mathematical Logic, 1879--1931. Harvard University Press, Cambridge, MA.
• 308: van Leeuwen, J., Ed. 1990. In Handbook of Theoretical Computer Science. vol. B: Formal Models and Semantics. Elsevier and MIT Press, Amsterdam, The Netherlands, and Cambridge, MA.
• 309: Vanderbei, R. 2001. Linear Programming: Foundations and Extensions. Kluwer's International Series.
• 310: Wang, C., Ivančić, F., Ganai, M., and Gupta, A. 2005. Deciding separation logic formulae by SAT and incremental negative cycle elimination. In Proceedings of International Conference on Logic for Artificial Intelligence and Reasoning (LPAR). Number 3835 in Lecture Notes in Artificial Intelligence, vol. 3835. Springer-Verlag, Berlin, Germany, 322--336.
• 311: Weidenbach, C., Brahm, U., Hillenbrand, T., Keen, E., Theobalt, C., and Topic, D. 2002. SPASS version 2.0. In Proceedings of the 18th International Conference on Automated Deduction—CADE-18. Lecture Notes in Computer Science, vol. 2392. Springer-Verlag, Berlin, Germany, 275--279.
• 312: Weld, D. and Wolfman, S. 1999. The LPSAT system and its application to resource planning. In Proceedings 16th International Joint Conference on Artificial Intelligence (IJCAI).
• 313: Wenzel, M. 1999. Isar—A generic interpretative approach to readable formal proof documents. In Proceedings of the 12th International Conference on Theorem Proving in Higher Order Logics, TPHOLs'99. Lecture Notes in Computer Science, vol. 1690. Springer-Verlag, Berlin, Germany, 167--184.
• 314: Weyhrauch, R. W. 1980. Prolegomena to a theory of mechanized formal reasoning. Artif. Intell. 13, 1 and 2 (Apr.), 133--170.
• 315: Weyhrauch, R. W. and Thomas, A. J. 1974. FOL: A proof checker for first order logic. Tech. rep. AIM-235. Computer Science Department, Artificial Intelligence Laboratory, Stanford Univ., Stanford, CA.
• 316: Wies, T., Kuncak, V., Zee, K., Podelski, A., and Rinard, M. C. 2006. On verifying complex properties using symbolic shape analysis. CoRR abs/cs/0609104. informal publication.
• 317: Williams, H. P. 1976. Fourier-Motzkin elimination extension to integer programming problems. J. Comb. Theory, Ser. A 21, 1, 118--123.
• 318: Yoeli, M., Ed. 1990. Formal Verification of Hardware Design. IEEE Computer Society Press, Los Alamitos, CA.
• 319: Zermelo, E. 1908. Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen 59, 261--281. (Translation by van Heijenoort in From Frege to Gödel.)
• 320: Zhang, H. 1997. SATO: An efficient propositional prover. In Proceedings of the Conference on Automated Deduction. Springer-Verlag, Berlin, Germany, 272--275.
• 321: Zhang, L. and Malik, S. 2002. The quest for efficient boolean satisfiability solvers. In Proceedings of the 19th International Conference on Automated Deduction CADE-19, Springer-Verlag, Berlin, Germany.
• 322: Zhang, L. and Malik, S. 2003. Validating SAT solvers using an independent resolution-based checker: Practical implementations and other applications. In Proceedings of the 2003 Design, Automation and Test in Europe Conference and Exposition (DATE 2003). IEEE Computer Society Press, Los Alamitos, CA, 10880--10885.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
      F.4.1 Mathematical Logic

Additional Classification:
  I. Computing Methodologies
  I.2 ARTIFICIAL INTELLIGENCE
      I.2.3 Deduction and Theorem Proving

General Terms:
Theory, Verification