References

  1. Michaël Armand, Germain Faure, Benjamin Grégoire, Chantal Keller, Laurent Thery & Benjamin Werner (2011): A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses. In: CPP '11, LNCS 7086. Springer, pp. 135–150, doi:10.1007/978-3-642-25379-9_12.
  2. Gilles Audemard & Laurent Simon (2009): Predicting Learnt Clauses Quality in Modern SAT Solvers. In: IJCAI '09. IJCAI Organization, pp. 399–404.
  3. Armin Biere (2012): Lingeling and Friends Entering the SAT Challenge 2012. In: Proc. SAT Challenge 2012, Department of Computer Science Series of Publications B B-2012-2. University of Helsinki, pp. 33–34.
  4. Sascha Böhme, Anthony Fox, Thomas Sewell & Tjark Weber (2011): Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. In: CPP '11, LNCS 7086. Springer, pp. 183–198, doi:10.1007/978-3-642-25379-9_15.
  5. Robert S. Boyer & Warren A. Hunt, Jr. (2006): Function Memoization and Unique Object Representation for ACL2 Functions. In: ACL2 '06. ACM, pp. 81–89, doi:10.1145/1217975.1217992.
  6. Robert S. Boyer & J Strother Moore (2002): Single-Threaded Objects in ACL2. In: PADL '02, LNCS 2257. Springer, pp. 9–27, doi:10.1007/3-540-45587-6_3.
  7. Aaron R. Bradley (2012): Understanding IC3. In: SAT '12, LNCS 7317. Springer, pp. 1–14, doi:10.1007/978-3-642-31612-8_1.
  8. Robert Brayton & Alan Mishchenko (2010): ABC: An Academic Industrial-Strength Verification Tool. In: CAV '10, LNCS 6174. Springer, pp. 24–40, doi:10.1007/978-3-642-14295-6_5.
  9. Robert Brummayer & Armin Biere (2006): Local Two-Level And-Inverter Graph Minimization without Blowup. In: MEMICS '06.
  10. Robert Brummayer & Armin Biere (2009): Fuzzing and Delta-Debugging SMT Solvers. In: SMT '09. ACM, pp. 1–5, doi:10.1145/1670412.1670413.
  11. Satrajit Chatterjee, Alan Mishchenko, Robert Brayton & Andreas Kuehlmann (2007): On resolution proofs for combinational equivalence. In: DAC '07. ACM, pp. 600–605, doi:10.1145/1278480.1278631.
  12. Ashish Darbari, Bernd Fischer & Jotilde07Eao Marques-Silva (2010): Industrial-Strength Certified SAT Solving through Verified SAT Proof Checking. In: ICTAC '10, LNCS 6255. Springer, pp. 260–274, doi:10.1007/978-3-642-14808-8_18.
  13. Jared Davis (2004): Finite Set Theory based on Fully Ordered Lists. In: ACL2 '04.
  14. Niklas Eén, Alan Mishchenko & Robert K. Brayton (2011): Efficient implementation of property directed reachability. In: FMCAD '11. FMCAD, Inc., pp. 125–134.
  15. Niklas Eén, Alan Mishchenko & Niklas Sörensson (2007): Applying Logic Synthesis for Speeding Up SAT. In: SAT '07, LNCS 4501. Springer, pp. 272–286, doi:10.1007/978-3-540-72788-0_26.
  16. Niklas Eén & Niklas Sörensson (2003): An Extensible SAT-solver. In: SAT '03, LNCS 2919. Springer, pp. 502–518, doi:10.1007/978-3-540-24605-3_37.
  17. Anthony Fox (2011): LCF-Style Bit-Blasting in HOL4. In: ITP '11, LNCS. Springer, pp. 357–362, doi:10.1007/978-3-642-22863-6_26.
  18. Michael J. Gordon, Arthur J. Milner & Christopher P. Wadsworth (1979): Edinburgh LCF: A Mechanized Logic of Computation. LNCS 78. Springer, doi:10.1007/3-540-09724-4.
  19. David Greve (2009): Automated Reasoning with Quantified Formulae. In: ACL2 '09. ACM, pp. 110–113, doi:10.1145/1637837.1637855.
  20. Warren A. Hunt, Jr., Matt Kaufmann, Robert Bellarmine Krug, J Moore & Eric Whitman Smith (2005): Meta Reasoning in ACL2. In: TPHOLs '05, LNCS 3603. Springer, pp. 163–178, doi:10.1007/11541868_11.
  21. Warren A. Hunt, Jr., Sol Swords, Jared Davis & Anna Slobodová (2010): Use of Formal Verification at Centaur Technology. In: David Hardin: Design and Verification of Microprocessor Systems for High-Assurance Applications. Springer, pp. 65–88, doi:10.1007/978-1-4419-1539-9_3.
  22. Matt Kaufmann & J Strother Moore (2011): How Can I Do That with ACL2? Recent Enhancements to ACL2. In: ACL2 '11, pp. 46–60, doi:10.4204/EPTCS.70.4.
  23. Filip Mari\'c (2009): Formalization and Implementation of Modern SAT Solvers. Journal of Automated Reasoning 43(1), pp. 81–119, doi:10.1007/s10817-009-9127-8.
  24. Alan Mishchenko, Michael Case, Robert Brayton & Stephen Jang (2008): Scalable and scalably-verifiable sequential synthesis. In: ICCAD '08. IEEE, pp. 234–241, doi:10.1109/ICCAD.2008.4681580.
  25. Alan Mishchenko, Satrajit Chatterjee & Robert Brayton (2006): DAG-Aware AIG Rewriting: A Fresh Look at Combinational Logic Synthesis. In: DAC '06. ACM, pp. 532–535, doi:10.1145/1146909.1147048.
  26. Alan Mishchenko, Satrajit Chatterjee, Roland Jiang & Robert Brayton (2005): FRAIGs: A Unifying Representation for Logic Synthesis and Verification. Technical Report. EECS Dept., UC Berkeley.
  27. Duckki Oe, Aaron Stump, Corey Oliver & Kevin Clancy (2012): versat: A Verified Modern SAT Solver. In: VMCAI '12, LNCS 7148. Springer, pp. 363–378, doi:10.1007/978-3-642-27940-9_24.
  28. Sol Swords & Jared Davis (2011): Bit-Blasting ACL2 Theorems. In: ACL2 '11, Electronic Proceedings in Theoretical Computer Science 70, pp. 84–102, doi:10.4204/EPTCS.70.7.
  29. Sol Swords & Warren A. Hunt, Jr. (2010): A Mechanically Verified AIG to BDD Conversion Algorithm. In: ITP '10, LNCS 6172. Springer, pp. 435–449, doi:10.1007/978-3-642-14052-5_30.
  30. G. S. Tseitin (1968): On the Complexity of Derivation in Propositional Calculus. Zapiski nauchnykh seminarov LOMI 8, pp. 234–259, doi:10.1007/978-3-642-81955-1_28. English translation of this volume: Consultants Bureau, N.Y., 1970, pp. 115–125.
  31. Tjark Weber & Hasan Amjad (2009): Efficiently Checking Propositional Refutations in HOL Theorem Provers. Journal of Applied Logic 7(1), pp. 26–40, doi:10.1016/j.jal.2007.07.003.
  32. Nathan Wetzler, Marijn J. H. Heule & Warren A. Hunt, Jr. (2013): Mechanical Verification of SAT Refutations with Extended Resolution. In: To appear in ITP 2013.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org