# ACL2 support for verification projects

Conference paper

First Online:

## Abstract

This talk discusses the use of a particular theorem prover, ACL2, on formal verification projects, particularly in industrial settings. In addition to describing briefly some existing and ongoing applications of ACL2, I'll discuss features relevant to formal verification projects.

## Keywords

Theorem Prover Automate Reasoning Formal Verification Proof Obligation Computational Logic
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

## Preview

Unable to display preview. Download preview PDF.

## References

- 1.Argonne National Laboratory, Mathematics and Computer Science Division. A Summary of New Results in Mathematics Obtained with Argonne's Automated Deduction Software. URL http://www-c.mcs.anl.gov/home/mccune/ar/-new_results/index.htmlGoogle Scholar
- 2.D. Basin and M. Kaufmann. The Boyer-Moore Prover and Nuprl: An Experimental Comparison. In:
*Proceedings of the First Workshop on “Logical Frameworks”*, Antibes, France, May 1990. See also Technical Report 58, Computational Logic, Inc., URL ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/058.ps or http://www.cli.com/reports/.Google Scholar - 3.M. Bickford and D. Jamsek. Formal specification and verification of VHDL. In
*Proceedings of Formal Methods in Computer-Aided Design (FMCAD'96)*, M. Srivas and A. Camilleri (eds.), Springer-Verlag, November, 1996Google Scholar - 4.W. Bledsoe. A maximal method for set variables in automatic theorem-proving. In
*Machine Intelligence 9*, ed. J. E. Hayes, D. Michie, and L. I. Mikulich. Ellis Harwood Ltd., Chichester, 1979, pp. 53–100.Google Scholar - 5.W. Bledsoe. A resolution-based prover for general inequalities. Technical Report ATP-52, University of Texas, Austin, July 1979.Google Scholar
- 6.R. Boyer. Nqthm Bibliography. URL ftp://ftp.cs.utexas.edu/pub/boyer/-nqthm/nqthm-bibliography.html.Google Scholar
- 7.R. Boyer, D. Goldschlag, M. Kaufmann, and J Moore. Functional Instantiation in First Order Logic. In
*Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy*, Academic Press, 1991, pp. 7–26.Google Scholar - 8.R. Boyer, M. Kaufmann, and J Moore. The Boyer-Moore Theorem Prover and Its Interactive Enhancement.
*Computers and Mathematics with Applications*, 5(2) (1995) pp. 27–62.CrossRefMathSciNetGoogle Scholar - 9.R. Boyer and J Moore.
*A Computational Logic*, Academic Press: New York, 1979.zbMATHGoogle Scholar - 10.R. Boyer and J Moore. Integrating Decision Procedures into Heuristic Theorem Provers: A Case Study of Linear Arithmetic, In
*Machine Intelligence 11*, Oxford University Press, 1988, pp. 83–124.Google Scholar - 11.R. Boyer and J Moore. Mechanized Formal Reasoning about Programs and Computing Machines. In R. Veroff (ed.),
*Automated Reasoning and Its Applications: Essays in Honor of Larry Wos*, MIT Press, 1996.Google Scholar - 12.R. Boyer and J Moore.
*A Computational Logic Handbook*,*Second Edition*. Academic Press: London, 1997.Google Scholar - 13.B. Brock. Defstructure for ACL2. URL http://www.cs.utexas.edu/users/-moore/acl2/reports/b97.ps.Google Scholar
- 14.B. Brock and W. Hunt, Jr. The Dual-Eval Hardware Description Language and Its Use in the Formal Specification and Verification of the FM9001 Microprocessor.
*Formal Methods in System Design*, Kluwer Academic Publishers. Volume 11, Issue 1, July, 1997, pp. 71–104.Google Scholar - 15.B. Brock and W. Hunt, Jr. Formally Specifying and Mechanically Verifying Programs for the Motorola Complex Arithmetic Processor DSP. 1997 IEEE InternationalConference on Computer Design, Austin, TX, October 1997, pp. 31–36.Google Scholar
- 16.B. Brock, M. Kaufmann, and J Moore. ACL2 Theorems about Commercial Microprocessors. In
*Proceedings of Formal Methods in Computer-Aided Design (FM-CAD'96)*, M. Srivas and A. Camilleri (eds.), Springer-Verlag, November, 1996, pp. 275–293.Google Scholar - 17.R. Bryant. Graph Based Algorithms for Boolean Function Manipulation.
*IEEE Trans. Comp.*,**C-35**(8), August 1986.Google Scholar - 18.S-C. Chou
*Mechanical Geometry Theorem Proving*D. Reidel, 1988.Google Scholar - 19.E. Clarke and X. Zhao. Analytica: A Theorem Prover for Mathematica. The Journal of Mathematica
**3**(1), 56–71, Winter 1993.Google Scholar - 20.CMU — School of Computer Science.
*Model Checking at CMU*. URL http://-www.cs.cmu.edu/~modelcheck/.Google Scholar - 21.W. Farmer, J. Guttman, and F. J. Thayer. IMPS: An Interactive Mathematical Proof System. J. Automated Reasoning,
**11**(2), 213–248, 1993.CrossRefzbMATHGoogle Scholar - 22.R. Gamboa. Defthms About Zip and Tie: Reasoning About Powerlists in ACL2. University of Texas Computer Sciences Technical Report No. TR97-02.Google Scholar
- 23.R. Gamboa. Mechanically Verifying the Correctness of the Fast Fourier Transform in ACL2. To appear in
*Third International Workshop on Formal Methods for Parallel Programming: Theory and Applications (FMPPTA)*, Orlando, FL, 1998. URL http://www.lim.com/~ruben/research/papers/fft. html.Google Scholar - 24.M. Gordon and T. Melham (editors).
*Introduction to HOL: A Theorem Proving Environment for Higher-Order Logic*. Cambridge University Press, 1993.Google Scholar - 25.D. Greve,M. Wilding, and D. Hardin. Efficient Simulation Using a Simple Formal Processor Model. April, 1998, Rockwell Collins Advanced Technology Center (submitted for publication).Google Scholar
- 26.D. Guaspari, C. Marceau, and W. Polak. Formal verification of Ada programs. IEEE Trans. Software Engineering, vol. 16, 1990, pp. 1058–1075.CrossRefGoogle Scholar
- 27.L. Hines. Struve: The Strive-based Subset Prover.
*Proc. 10th Int'l Conf. Automated Deduction*, July 1990, Kaiserslautern, Germany, Springer-Verlag, pp. 193–206.Google Scholar - 28.L. Hines. Strive and integers. In
*Proc. 12th Int'l Conf. Automated Deduction*, June 1992, Nancy, France, Springer-Verlag (192), pp. 416–430.Google Scholar - 29.G. Huet, G. Kahn, and C. Paulin-Mohring.
*The Coq Proof Assistant — A tutorial, Version 6.1*. Technical Report No. 204, INRIA, August 1997 (revised version distributed with Coq). See also URL http://pauillac.inria.fr/coq/.Google Scholar - 30.J-Y. Jang, S. Qadeer, M. Kaufmann, and C Pixley. Formal Verification of FIRE: A Case Study. In:
*Proceedings of Design Automation Conference (DAC)*, 1997, pp. 173–177.Google Scholar - 31.D. Kapur and H. Zhang. An Overview of Rewrite Rule Laboratory (RRL).
*J. Computer and Mathematics with Applications*,**29**(2), 1995, pp. 91–114.CrossRefMathSciNetGoogle Scholar - 32.M. Kaufmann. Response to FM91 Survey of Formal Methods: Nqthm and Pc-Nqthm. Technical Report 75, Computational Logic, Inc., March, 1992. URL ftp://ftp.cs.utexas.edu/pub/boyer/cli-reports/075.ps or http://-www.cli.com/reports/.Google Scholar
- 33.M. Kaufmann. Development and Verification of Year 2000 Conversion Rules using the ACL2 Theorem Prover.
*In preparation*.Google Scholar - 34.M. Kaufmann and J S. Moore.
*ACL2: A Computational Logic for Applicative Common Lisp, The User's Manual*. http://www.cs.utexas.edu/users/moore/-acl2/acl2-doc.html#User's-Manual.Google Scholar - 35.M. Kaufmann and J Moore. Design Goals for ACL2. In
*Proceedings of: Third International School and Symposium on Formal Techniques in Real Time and Fault Tolerant Systems*, Kiel, Germany (1994), pp. 92–117. Published by Christian-Albrechts-Universitat. See also Technical Report 101, Computational Logic, Inc. URL http: //www.cs.utexas.edu/users/moore/acl2/reports/km94.ps.Google Scholar - 36.M. Kaufmann and J Moore. An Industrial Strength Theorem Prover for a Logic Based on Common Lisp. In
*IEEE Transactions on Software Engineering***23**(4), April, 1997, pp. 203–213.CrossRefGoogle Scholar - 37.M. Kaufmann and J Moore. A Precise Description of the ACL2 Logic. URL http://www.cs.utexas.edu/users/moore/acl2/reports/km97a.ps.Google Scholar
- 38.M. Kaufmann and J Moore. Structured Theory Development for a Mechanized Logic. In preparation. (Earlier version entitled “High-Level Correctness of ACL2: A Story,” September, 1995, is distributed with ACL2 release; see http://-www.cs.utexas.edu/users/moore/acl2/.Google Scholar
- 39.M. Kaufmann and P. Pecchiari. Interaction with the Boyer-Moore Theorem Proven A Tutorial Study Using the Arithmetic-Geometric Mean Theorem.
*Journal of Automated Reasoning*16, no. 1–2 (1996) 181–222.MathSciNetCrossRefzbMATHGoogle Scholar - 40.W. McCune. Otter: An Automated Deduction System. URL http://www-c.mcs.-anl.gov/home/mccune/ar/otter.Google Scholar
- 41.W. McCune. Solution of the Robbins Problem. J. Automated Reasoning 19(3), 263–276 (1997).zbMATHCrossRefMathSciNetGoogle Scholar
- 42.J Moore. An ACL2 Proof of Write Invalidate Cache Coherence. To appear in Proceedings of Computer Aided Verification, CAV'98, Vancouver, June 28–July 2, 1998, Lecture Notes in Computer Science.Google Scholar
- 43.J Moore, T. Lynch, and M. Kaufmann. A Mechanically Checked Proof of the AMD5K86 Floating-Point Division Program. To appear,
*IEEE Trans. Comp.*See also URL http: //devil.ece.utexas.edu/~lynch/divide/divide.html.Google Scholar - 44.S. Owre, J. Rushby, and N. Shankar. Integration in PVS: Tables, types, and model checking. In Ed Brinksma, editor,
*Tools and Algorithms for the Construction and Analysis of Systems (TACAS '97)*, number 1217 in Lecture Notes in Computer Science, Springer-Verlag, Enschede, The Netherlands, April 1997, pp. 366–383.Google Scholar - 45.J. Park, C. Pixley, and H. Cho. An Efficient Logic Equivalence Checker for Industrial Circuits. Submitted.Google Scholar
- 46.J. Rushby. Automated deduction and formal methods. In Rajeev Alur and Thomas A. Henzinger, editors,
*Proceedings of the 8th International Conference on Computer Aided Verification*, number 1102 in Lecture Notes in Computer Science, Springer-Verlag, New Brunswick, NJ, July 1996, pp. 169–183.Google Scholar - 47.D. Russinoff. A Mechanically Checked Proof of IEEE Compliance of the AMD-K5
^{TM}Floating-Point Square Root Microcode. To appear,*Formal Methods in System Design*. URL http://www.onr.com/user/russ/david/fsqrt.html.Google Scholar - 48.D. Russinoff. A Mechanically Checked Proof of IEEE Compliance of the Floating Point Multiplication, Division, and Square Root Algorithms of the AMD-K7
^{™}Processor. URL http://www.onr.com/user/russ/david/k7-div-sqrt.html.Google Scholar - 49.D. Russinoff. A Case Study in Formal Verification of Register-Transfer Logic: The Floating Point Adder of the AMD-K7
^{TW}Processor. In final preparation.Google Scholar - 50.J. Sawada and W. Hunt, Jr. Trace Table Based Approach for Pipelined Micro-processor Verification. In Proceedings of Computer Aided Verification, CAV'97, Lecture Notes in Computer Science 1254, Springer Verlag, 1997, pp. 364–375.Google Scholar
- 51.J. Sawada and W. Hunt, Jr. Processor Verification with Precise Exceptions and Speculative Execution. To appear in Proceedings of Computer Aided Verification, CAV'98, Vancouver, June 28–July 2, 1998, Lecture Notes in Computer Science.Google Scholar
- 52.N. Shankar. Unifying verification paradigms. In Bengt Jonsson and Joachim Parrow, editors,
*Formal Techniques in Real-Time and Fault-Tolerant Systems*, volume 1135 of Lecture Notes in Computer Science, Springer-Verlag, Uppsala, Sweden, September 1996, pp. 22–39. See also URL http://www.csl.sri.com/-ftrtft96.html.Google Scholar - 53.M. Smith. Top-level README for IACL2 (Infix ACL2). URL http://-www.cs.utexas.edu/users/moore/infix/README.html, April, 1997.Google Scholar
- 54.G. Steele, Jr.
*Common Lisp The Language*,*Second Edition*. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.zbMATHGoogle Scholar - 55.The VIS Group. VIS: A system for Verification and Synthesis. In Rajeev Alur and Thomas A. Henzinger, editors,
*Proceedings of the 8th International Conference on Computer Aided Verification*, number 1102 in Lecture Notes in Computer Science, Springer-Verlag, New Brunswick, NJ, July 1996, pp. 428–432. See also URL: http://www-cad.eecs.berkeley.edu/Respep/Research/vis/.Google Scholar - 56.M. Wilding. Robust Computer System Proofs in PVS. In C. Michael Holloway and Kelly J. Hayhurst, editors,
*LFM97: Fourth NASA Langley Formal Methods Workshop*, NASA Conference Publication, 1997. See also URL http://atb-www.-larc.nasa.gov/Lfm97/.Google Scholar - 57.W. Young. Comparing Verification Systems: Interactive Consistency in ACL2. In:
*Proceedings of the Eleventh Annual Conference on Computer Assurance*, 1996, pp. 35–45. An expanded version appears in*IEEE Transactions on Software Engineering*, Vol. 23, no. 4, (April, 1997) pp. 214–223. See also URL http://www.cs.-utexas.edu/users/moore/acl2/reports/y96a.ps.Google Scholar - 58.W. Young. The Specification of a Simple Autopilot in ACL2. URL http://www.-cs.utexas.edu/users/moore/acl2/reports/y96b.ps.Google Scholar
- 59.Y. Yu.
*Automated Proofs of Object Code for a Widely used Microprocessor*. Technical Report 92, Computational Logic, Inc., May, 1993. URL http://www.cli.-com/reports/files/92.ps.Google Scholar

## Copyright information

© Springer-Verlag Berlin Heidelberg 1998