Integrating external deduction tools with ACL2

M. Kaufmann, J S. Moore, S. Ray, E. Reeber, Integrating external deduction tools with ACL2, in: C. Benzmüller, B. Fischer, G. Sutcliffe (Eds.), Proceedings of the 6th International Workshop on Implementation of Logics (IWIL 2006), CEUR Workshop Proceedings, vol. 212, 2006, pp. 7–26 McMillan, 1993 Moskewicz, 2001, Chaff: Engineering an efficient SAT solver, 530 Kaufmann, 2000 Kaufmann M. Kaufmann, J S. Moore, Design goals of ACL2, Tech. Rep. 101, Computational Logic Incorporated (CLI), 1717 West Sixth Street, Suite 290, Austin, TX 78703, 1994 J S. Moore, 1998, A mechanically checked proof of the kernel of the AMD5K86 floating-point division algorithm, IEEE Transactions on Computers, 47, 913, 10.1109/12.713311 Russinoff, 1998, A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions, LMS Journal of Computation and Mathematics, 1, 148, 10.1112/S1461157000000176 Russinoff, 2000, RTL verification: A floating point multiplier, 201 A. Flatau, M. Kaufmann, D.F. Reed, D. Russinoff, E.W. Smith, R. Sumners, Formal verification of microprocessors at AMD, in: M. Sheeran, T.F. Melham (Eds.), 4th International Workshop on Designing Correct Circuits (DCC 2002), Grenoble, France, 2002 Brock, 1997, Formally specifying and mechanically verifying programs for the Motorola complex arithmetic processor DSP, 31 D.A. Greve, R. Richards, M. Wilding, A summary of intrinsic partitioning verification, in: M. Kaufmann, J S. Moore (Eds.), 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, 2004 Kaufmann, 2001, Structured theory development for a mechanized logic, Journal of Automated Reasoning, 26, 161, 10.1023/A:1026517200045 Boyer, 1981, Metafunctions: Proving them correct and using them efficiently as new proof procedure, 103 Kaufmann Church, 1937, Formal definitions in the theory of ordinal numbers, Fundamenta Mathematicae, 28, 11, 10.4064/fm-28-1-11-21 Rogers, 1987 Manolios, 2003, Algorithms for ordinal arithmetic, vol. 2741, 243 Boyer, 1991, Functional instantiation in first order logic, 7 W.J. Legato, Generic theories as proof strategies: A case study for weakest precondition style proofs, in: M. Kaufmann, J S. Moore (Eds.), 5th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2004), Austin, TX, 2004 Ray, 2004, Proof styles in operational semantics, vol. 3312, 67 Matthews, 2006, Verification condition generation via theorem proving, vol. 4246, 362 1993 Nipkow, 2002, Isabelle/HOL: A Proof Assistant for Higher Order Logics, vol. 2283 Kaufmann, 2000, Modular proof: The fundamental theorem of calculus, 59 Steele, 1990 Hunt, 2005, Meta reasoning in ACL2, vol. 3603, 163 J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, Tech. Rep. CRC-053, SRI International Cambridge Computer Science Research Center, 1995 S. Ray, J. Matthews, M. Tuttle, Certifying compositional model checking algorithms in ACL2, in: W.A. Hunt Jr., M. Kaufmann, J S. Moore (Eds.), 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2 2003), Boulder, CO, 2003 Reeber, 2006, A SAT-based decision procedure for the subclass of unrollable list formulas in ACL2 (SULFA), vol. 4130, 453 Manolios, 2004, Automatic verification of safety and liveness of xscale-like processor models using WEB refinements, 168 Manolios, 2005, Refinement maps for efficient verification of processor models, 1304 Burger, 2004, Scaling to the end of silicon with EDGE architectures, IEEE Computer, 37, 44, 10.1109/MC.2004.65 Hunt, 2005, Formalization of the DE2 language, 20 Ranise Brock, 1997, The dual-eval hardware description language, Formal Methods in Systems Design, 11, 71, 10.1023/A:1008685826293 Russinoff, 1995, A formalization of a subset of VHDL in the Boyer–Moore logic, Formal Methods in Systems Design, 7, 7, 10.1007/BF01383871 Gordon, 1995, The semantic challenges of Verilog HDL, 136 Sawada, 2006, ACL2SIX: A hint used to integrate a theorem prover and an automated verification tool, 161 Mony, 2004, Scalable automated verification via exper-system guided transformations, vol. 3312, 217 Gunter, 1998, Adding external decision procedures to HOL90 securely, vol. 1479, 143 Müller, 1995, Combining model checking and deduction of I/O-automata, vol. 1019, 1 J.D. Guttman, A proposed interface logic for verification environments, Tech. Rep. M-91-19, The Mitre Corporation, Mar. 1991 Rajan, 1995, An integration of model-checking with automated proof checking, vol. 939, 84 Shankar, 2001, Using decision procedures with higher order logics, vol. 2152, 5 Basin, 2000, Combining WS1S and HOL, 39 Dennis, 2000, The PROSPER toolkit, vol. 1785, 78 Gordon, 2002, Programming combinations of deduction and BDD-based symbolic calculation, LMS Journal of Computation and Mathematics, 5, 56, 10.1112/S1461157000000693 Meng, 2004, Experiments on supporting interactive proof using resolution, vol. 3097, 372 Hurd, 2002, An LCF-style interface between HOL and first-order logic, vol. 2392, 134 McCune, 2000, Ivy: A preprocessor and proof checker for first-order logic, 217 M. Kaufmann, J S. Moore, Should we begin a standardization process for interface logics?, Tech. Rep. 72, Computational Logic Inc. (CLI), Jan. 1992 Gordon, 2006, An integration of HOL and ACL2, 153