A Parallelized Theorem Prover for a Logic with Parallel Execution

1. Kaufmann, M., Manolios, P., Moore, J. S : Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers, Boston (2000)

   Google Scholar 

2. Brock, B., Kaufmann, M., Moore, J. S : ACL2 theorems about commercial microprocessors. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 275–293. Springer, Heidelberg (1996)

   Google Scholar 

3. Russinoff, D., Kaufmann, M., Smith, E., Sumners, R.: Formal verification of floating-point RTL at AMD using the ACL2 theorem prover. In: Nikolai, S. (ed.) Proceedings of the 17th IMACS World Congrress on Scientific Computation, Applied Mathematics and Simulation, Paris, France (2005)

   Google Scholar 

4. Hunt Jr., W.A., Swords, S., Davis, J., Slobodova, A.: Use of formal verification at Centaur Technology. In: Hardin, D.S. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 65–88. Springer, US (2010)

   Chapter  Google Scholar 

5. ACL2: ACL2 Version 6.0 Documentation (December 2012), http://www.cs.utexas.edu/users/moore/acl2/v6-0/acl2-doc.html#User's-Manual

6. Rager, D.L.: Implementing a parallelism library for ACL2 in modern day Lisps. Master’s thesis, The University of Texas at Austin (2008)

   Google Scholar 

7. Rager, D.L., Hunt Jr., W.A.: Implementing a parallelism library for a functional subset of Lisp. In: Proceedings of the 2009 International Lisp Conference, pp. 18–30. Association of Lisp Users, Sterling (2009)

   Google Scholar 

8. ACL2 Community Books, https://code.google.com/p/acl2-books/

9. Rager, D.L.: ACL2 6.0 regression suite test configuration details, http://www.cs.utexas.edu/users/ragerdl/papers/itp2013/

10. Moore, J. S , Porter, G.: The apprentice challenge. ACM Transactions on Programming Languages and Systems 24, 193–216 (2002)

    Google Scholar 

11. Verbeek, F., Schmaltz, J.: Formal verification of a deadlock detection algorithm. In: Hardin, D., Schmaltz, J. (eds.) Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications, Austin, Texas, USA, November 3-4. Electronic Proceedings in Theoretical Computer Science, vol. 70, pp. 103–112. Open Publishing Association (2011)

    Google Scholar 

12. Rager, D.L.: Parallelizing an Interactive Theorem Prover: Functional Programming and Proofs with ACL2. PhD thesis, The University of Texas at Austin (2012)

    Google Scholar 

13. Moten, R.: Exploiting parallelism in interactive theorem provers. In: Grundy, J., Newey, M. (eds.) TPHOLs 1998. LNCS, vol. 1479, pp. 315–330. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

14. Meseguer, J., Winkler, T.C.: Parallel programmming in Maude. In: Banâtre, J.-P., Le Métayer, D. (eds.) Research Directions in High-Level Parallel Programming Languages 1991. LNCS, vol. 574, pp. 253–293. Springer, Heidelberg (1992)

    Chapter  Google Scholar 

15. Bonacina, M.P., McCune, W.: Distributed theorem proving by peers. In: Bundy, A. (ed.) CADE 1994. LNCS, vol. 814, pp. 841–845. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

16. Kapur, D., Vandevoorde, M.T.: DLP: a paradigm for parallel interactive theorem proving (1996)

    Google Scholar 

17. Schumann, J., Letz, R.: PARTHEO: A high-performance parallel theorem prover. In: Stickel, M.E. (ed.) CADE 1990. LNCS, vol. 449, pp. 40–56. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

18. Schumann, J.: SicoTHEO: Simple competitive parallel theorem provers. In: McRobbie, M.A., Slaney, J.K. (eds.) CADE 1996. LNCS, vol. 1104, pp. 240–244. Springer, Heidelberg (1996)

    Chapter  Google Scholar 

19. Matthews, D.C.J., Wenzel, M.: Efficient parallel programming in poly/ML and isabelle/ML. In: DAMP 2010: Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, pp. 53–62. ACM, New York (2010)

    Chapter  Google Scholar 

20. Wenzel, M.: Parallel proof checking in Isabelle/Isar. In: Reis, G.D., Théry, L. (eds.) ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS). ACM Digital library (August 2009)

    Google Scholar 

21. Wenzel, M.: Shared-memory multiprocessing for interactive theorem proving. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 418–434. Springer, Heidelberg (2013)

    Google Scholar 

22. Boyer, R.S., Moore, J.S.: A Computational Logic Handbook. Academic Press, New York (1988)

    MATH  Google Scholar 

23. Kaufmann, M., Wilding, M.: A parallel version of the Boyer-Moore prover. Technical Report 39. Computational Logic, Inc. (February 1989)

    Google Scholar 

24. Halstead Jr., R.H.: Implementation of multilisp: Lisp on a microprocessor. In: Conference on Lisp and Functional Programming, pp. 9–17 (1984)

    Google Scholar 

25. Goldman, R., Gabriel, R.P., Sexton, C.: Qlisp: An interim report. In: Ito, T., Halstead Jr., R.H. (eds.) US/Japan WS 1989. LNCS, vol. 441, pp. 161–181. Springer, Heidelberg (1990)

    Chapter  Google Scholar 

26. Harrison, W.L.: The interprocedural analysis and automatic parallelization of scheme programs. Lisp and Symbolic Computation 2(3), 179–396 (1989)

    Article  Google Scholar 

27. Harrison, W.L., Ammarguellat, Z.: A comparison of automatic versus manual parallelization of the Boyer-Moore theorem prover. In: Selected Papers of the Second Workshop on Languages and Compilers for Parallel Computing, pp. 307–330. Pitman Publishing, London (1990)

    Google Scholar 

28. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)

    Google Scholar 

29. University of Cambridge: HOL4 Kananaskis 5 (March 2010), http://hol.sourceforge.net/

30. Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) CADE 1992. LNCS, vol. 607, pp. 748–752. Springer, Heidelberg (1992)

    Google Scholar 

31. SRI International: PVS Specification and Verification System (July 2012), http://pvs.csl.sri.com/

32. Rager, D.L., Hunt Jr., W.A., Kaufmann, M.: A futures library and parallelism abstractions for a functional subset of Lisp. In: Proceedings of the 4th European Lisp Symposium (March 2011)

    Google Scholar 

33. Schumann, J.: Automated theorem proving in software engineering. Springer (2001)

    Google Scholar 

Download references