Hostname: page-component-586b7cd67f-t7czq Total loading time: 0 Render date: 2024-11-28T17:28:49.076Z Has data issue: false hasContentIssue false
  • English
  • Français

Efficient execution in an automated reasoning environment

Part of: JFP Research Articles

Published online by Cambridge University Press:  01 January 2008

DAVID A. GREVE ,
MATT KAUFMANN ,
PANAGIOTIS MANOLIOS ,
J STROTHER MOORE ,
SANDIP RAY ,
JOSÉ LUIS RUIZ-REINA ,
ROB SUMNERS ,
DARON VROON  and
MATTHEW WILDING
DAVID A. GREVE
Affiliation:
Rockwell Collins Advanced Technology Center, Cedar Rapids, IA, USA
MATT KAUFMANN
Affiliation:
Department of Computer Sciences, University of Texas at Austin, Austin, TX, USA (url: http://www.cs.utexas.edu/users/kaufmann/)
PANAGIOTIS MANOLIOS
Affiliation:
College of Computing, Georgia Institute of Technology, Atlanta, GA, USA (url: http://www.cc.gatech.edu/home/manolios/)
J STROTHER MOORE
Affiliation:
Department of Computer Sciences, University of Texas at Austin, Austin, TX, USA (url: http://www.cs.utexas.edu/users/moore/)
SANDIP RAY
Affiliation:
Department of Computer Sciences, University of Texas at Austin, Austin, TX, USA (url: http://www.cs.utexas.edu/users/sandip/)
JOSÉ LUIS RUIZ-REINA
Affiliation:
Dep. de Ciencias de la Computación e Inteligencia Artificial, Univ. de Sevilla, Seville, Spain (url: http://www.cs.us.es/~jruiz/)
ROB SUMNERS
Affiliation:
Advanced Micro Devices, Inc., Sunnyvale, CA, USA
DARON VROON
Affiliation:
College of Computing, Georgia Institute of Technology, Atlanta, GA, USA (url: http://www.cc.gatech.edu/home/vroon/)
MATTHEW WILDING
Affiliation:
Rockwell Collins Advanced Technology Center, Cedar Rapids, IA, USA (url: http://hokiepokie.org/)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

We describe a method that permits the user of a mechanized mathematical logic to write elegant logical definitions while allowing sound and efficient execution. In particular, the features supporting this method allow the user to install, in a logically sound way, alternative executable counterparts for logically defined functions. These alternatives are often much more efficient than the logically equivalent terms they replace. These features have been implemented in the ACL2 theorem prover, and we discuss several applications of the features in ACL2.

Type
Articles
Information
Journal of Functional Programming , Volume 18 , Issue 1 , January 2008 , pp. 15 - 46
Copyright
Copyright © Cambridge University Press 2007

References

Allen, S., Constable, R., Howe, D. & Aitken, W. (1990) The semantics of reflected proof. In: Fifth Annual IEEE Symposium on Logic in Computer Science, Mitchell, J. (ed). IEEE Computer Society Press, pp. 95–105.Google Scholar
Bevier, W. R., Hunt, W. A. Jr., Moore, J S. & Young, W. D. (1989) Special issue on system verification. J. Automated Reasoning 5 (4), 409–530.Google Scholar
Boyer, R. S. & Moore, J S. (1975). Proving theorems about pure Lisp functions. J. ACM 22 (1), 129–144.CrossRefGoogle Scholar
Boyer, R. S. & Moore, J S. (1979). A Computational Logic. New York: Academic Press.Google Scholar
Boyer, R. S. & Moore, J S. (1981). Metafunctions: Proving them correct and using them efficiently as new proof procedures. Pages 103–184 of: Boyer, R. S. & Moore, J S. (eds), The Correctness Problem in Computer Science. New York: Academic Press.Google Scholar
Boyer, R. S. & Moore, J S. (1997) A Computational Logic Handbook, 2nd ed. New York: Academic Press.Google Scholar
Boyer, R. S. & Moore, J S. (2002) Single-threaded objects in ACL2. In: Practical Aspects of Declarative Languages : 4th International Symposium, PADL 2002, Krishnamurthi, S. & Ramakrishnan, C. R. (eds). Lecture Notes in Computer Science, vol. 2257. New York: Springer-Verlag. pp. 9–27 Available at: http://www.cs.utexas.edu/users/moore/publications/stobj/main.ps.ZCrossRefGoogle Scholar
Brock, B. & Hunt, W. A. Jr. (1999) Formal analysis of the Motorola CAP DSP. In: Industrial-Strength Formal Methods in Practice, Hinchey, M. & Bowen, J. (eds), New York: Springer-Verlag, pp. 81–116.CrossRefGoogle Scholar
Brock, B., Kaufmann, M. & Moore, J S. (1996) ACL2 theorems about commercial microprocessors. In: Proceedings of the 1st International Conference on Formal Methods in Computer-Aided Design (FMCAD 1996). Srivas, M. & Camilleri, A. (eds). LNCS, vol. 1166. New York: Springer-Verlag, pp. 275–293.Google Scholar
Cowles, J., Gamboa, R. & van Baalen, J. (2003) Using ACL2 arrays to formalize matrix algebra. In: Proceedings of the 4th International Workshop on the ACL2 Theorem Prover and Its Applications, Hunt, W. A. Jr., Kaufmann, M. & Moore, J S. (eds), Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/Google Scholar
Crow, J., Owre, S., Rushby, J., Shankar, N. & Stringer-Calvert, D. (2001) Evaluating, Testing, and Animating PVS Specifications. Tech. rept. Menlo Park, CA: Computer Science Laboratory, SRI International. Available at: http://www.csl.sri.com/users/rushby/papers/attach.pdfGoogle Scholar
Davis, J. (2004) Finite set theory based on fully ordered lists. In: Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/Google Scholar
Goldberg, J., Kautz, W., Mellear-Smith, P. M., Green, M., Levitt, K., Schwartz, R. & Weinstock, C. (1984) Development and Analysis of the Software Implemented Fault Tolerance (Sift) Computer. Tech. rept. NASA Contractor Report 172146. Hampton, VA: NASA Langley Research Center.Google Scholar
Gordon, M., Hurd, J. & Slind, K. (2003) Executing the formal semantics of the Accellera property specification language by mechanised theorem proving. In: Proceedings of the 12th International Conference on Correct Hardware Design and Verification Methods, Geist, D. (ed). Lecture Notes in Computer Science, vol. 2860. New York: Springer-Verlag, pp. 200–215.CrossRefGoogle Scholar
Greve, D. & Wilding, M. (2003) Using MBE to speed a verified graph pathfinder. In: Proceedings of the 4th International Workshop on the ACL2 Theorem Prover and Its Applications, Hunt, W. A. Jr., Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2003/Google Scholar
Greve, D., Wilding, M. & Hardin, D. (2000) High-speed, analyzable simulators. In: Computer-Aided Reasoning: ACL2 Case Studies, Kaufmann, M., Manolios, P. & Moore, J S. (eds). New York: Kluwer Academic Press, pp. 113–136.CrossRefGoogle Scholar
Greve, D. A., Kaufmann, M., Manolios, P., Moore, J S., Ray, S., Ruiz-Reina, J. L., Sumners, R., Vroon, D. & Wilding, M. (2006) Efficient Execution in an Automated Reasoning Environment. Tech. rept. TR-06-59. Department of Computer Sciences, University of Texas at Austin. Available at: http://www.cs.utexas.edu/users/moore/publications/acl2-papers.-html#UtilitiesGoogle Scholar
Harrison, J. (1995) Metatheory and Reflection in Theorem Proving: A Survey and Critique. Tech. rept. CRC-053. SRI International Cambridge Computer Science Research Centre. Available at: http://www.cl.cam.ac.uk/users/jrh/papers/reflect.htmlGoogle Scholar
Hunt, W. A. Jr. (1994) FM8501: A Verified Microprocessor. Lecture Notes in Artificial Intelligence, vol. 795. Yew York: Springer-Verlag.CrossRefGoogle Scholar
Kaufmann, M. & Moore, J S. (1997) A precise description of the ACL2 logic. Tech. rept. Department of Computer Sciences, University of Texas at Austin. See URL: http://www.cs.utexas.edu/users/moore/publications/acl2-papers.-html#Foundations.Google Scholar
Kaufmann, M. & Moore, J S. (2001) Structured theory development for a mechanized logic. J. Automated Reasoning 26 (2), 161–203.CrossRefGoogle Scholar
Kaufmann, M & Moore, J S. (2006) ACL2 Home Page. Available at: !http://www.cs.utexas.edu/users/moore/acl2Google Scholar
Kaufmann, M. & Sumners, R. (2002) Efficient rewriting of data structures in ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications, Borrione, D., Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/Google Scholar
Liu, H. & Moore, J S. (2003) Executable JVM model for analytical reasoning: A study. In: IVME '03: Proceedings of the 2003 Workshop on Interpreters, Virtual Machines and Emulators. Yew York: ACM Press, pp. 15–23.CrossRefGoogle Scholar
Manolios, P. & Kaufmann, M. (2002) Adding a total order to ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications, Borrione, D., Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/Google Scholar
Manolios, P. & Moore, J S. (2003) Partial functions in ACL2. J. Automated Reasoning 31 (2), 107–127.CrossRefGoogle Scholar
Manolios, P. & Vroon, D. (2003) Algorithms for ordinal arithmetic. In: 19th International Conference on Automated Deduction – CADE-19, Baader, F. (ed). Lecture Notes in Artificial Intelligence, vol. 2741. New York: Springer-Verlag, pp. 243–257.CrossRefGoogle Scholar
Manolios, P. & Vroon, D. (2004) Integrating reasoning about ordinal arithmetic into ACL2. Proceedings of the 5th International Conference on Formal Methods in Computer-Aided Design – FMCAD 2004. Lecture Notes in Computer Science, vol. 3312. New York: Springer-Verlag.Google Scholar
Manolios, P. & Vroon, D. (2006) Ordinal arithmetic: Algorithms and mechanization. J. Automated Reasoning, 34 (4), 1–37.Google Scholar
Matthews, J. & Vroon, D. (2004) Partial clock functions in ACL2. Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/Google Scholar
Moore, J S. (2003) Inductive assertions and operational semantics. In: Correct Hardware Design and Verification Methods – CHARME 2003, Geist, D. & Tronci, E. (eds). Lecture Notes in Computer Science, vol. 2860. New York: Springer-Verlag. pp. 289–303.CrossRefGoogle Scholar
Paulin-Mohring, C. & Werner, B. (1993) Synthesis of ML programs in the system Coq. J. Symbolic Comput., 15, 607–640.CrossRefGoogle Scholar
Ray, S. (2004) Attaching efficient executability to partial functions in ACL2. In: Proceedings of the 5th International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2004/Google Scholar
Ray, S. & Sumners, R. (2002) Verification of an in-place quicksort in ACL2. In: Proceedings of the 3rd International Workshop on the ACL2 Theorem Prover and Its Applications, Borrione, D., Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2002/Google Scholar
Ruiz-Reina, J. L., Martín, F. J., Alonso, J. A. & Hidalgo, M. J. (2006) Formal correctness of a quadratic unification algorithm. J. Automat. Reason., 37 (1-2), 67–92.CrossRefGoogle Scholar
Russinoff, D., Kaufmann, M., Smith, E. & Sumners, R. (July 2005) Formal verification of floating-point RTL at amd using the ACL2 theorem prover. In: Proceedings of the 17th IMACS World Congress on Scientific Computation, Applied Mathematics and Simulation, Simonov, N. (ed). Available at: http://sab.sscc.ru/imacs2005/papers/T2-I-94-1021.pdfGoogle Scholar
Russinoff, D. M. & Flatau, A. (2000) RTL verification: A floating-point multiplier. In: Computer-Aided Reasoning: ACL2 Case Studies, Kaufmann, M., Manolios, P. & Moore, J S. (eds). New York: Kluwer Academic Publishers. pp. 201–232.CrossRefGoogle Scholar
Shankar, N. (1994) Metamathematics, Machines, and Gödel's Proof. Cambridge: Cambridge University Press.CrossRefGoogle Scholar
Shankar, N. (1999) Efficiently Executing PVS. Project report. Menlo Park, CA: Computer Science Laboratory, SRI International,.Google Scholar
Steele, G. L. Jr. (1990) Common Lisp the Language. 2nd ed.Woburn, MA: Digital Press.Google Scholar
Sumners, R. (2000) Correctness proof of a BDD manager in the context of satisfiability checking. In: Proceedings of the 2nd International Workshop on the ACL2 Theorem Prover and Its Applications, Kaufmann, M. & Moore, J S. (eds). Available at: http://www.cs.utexas.edu/users/moore/acl2/workshop-2000/Google Scholar
Weyhrauch, R. (1980) Prolegomena to a theory of mechanized formal reasoning. Artif. Intell. J. 13 (1), 133–170.CrossRefGoogle Scholar
Submit a response

Discussions

No Discussions have been published for this article.