Advertisement

ACL2 support for verification projects

  • Matt Kaufmann
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

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.

Unable to display preview. Download preview PDF.

References

  1. 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. 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. 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. 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. 5.
    W. Bledsoe. A resolution-based prover for general inequalities. Technical Report ATP-52, University of Texas, Austin, July 1979.Google Scholar
  6. 6.
    R. Boyer. Nqthm Bibliography. URL ftp://ftp.cs.utexas.edu/pub/boyer/-nqthm/nqthm-bibliography.html.Google Scholar
  7. 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. 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. 9.
    R. Boyer and J Moore. A Computational Logic, Academic Press: New York, 1979.zbMATHGoogle Scholar
  10. 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. 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. 12.
    R. Boyer and J Moore. A Computational Logic Handbook, Second Edition. Academic Press: London, 1997.Google Scholar
  13. 13.
    B. Brock. Defstructure for ACL2. URL http://www.cs.utexas.edu/users/-moore/acl2/reports/b97.ps.Google Scholar
  14. 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. 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. 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. 17.
    R. Bryant. Graph Based Algorithms for Boolean Function Manipulation. IEEE Trans. Comp., C-35(8), August 1986.Google Scholar
  18. 18.
    S-C. Chou Mechanical Geometry Theorem Proving D. Reidel, 1988.Google Scholar
  19. 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. 20.
    CMU — School of Computer Science. Model Checking at CMU. URL http://-www.cs.cmu.edu/~modelcheck/.Google Scholar
  21. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 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. 33.
    M. Kaufmann. Development and Verification of Year 2000 Conversion Rules using the ACL2 Theorem Prover. In preparation.Google Scholar
  34. 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. 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. 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. 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. 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. 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. 40.
    W. McCune. Otter: An Automated Deduction System. URL http://www-c.mcs.-anl.gov/home/mccune/ar/otter.Google Scholar
  41. 41.
    W. McCune. Solution of the Robbins Problem. J. Automated Reasoning 19(3), 263–276 (1997).zbMATHCrossRefMathSciNetGoogle Scholar
  42. 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. 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. 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. 45.
    J. Park, C. Pixley, and H. Cho. An Efficient Logic Equivalence Checker for Industrial Circuits. Submitted.Google Scholar
  46. 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. 47.
    D. Russinoff. A Mechanically Checked Proof of IEEE Compliance of the AMD-K5TM 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. 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. 49.
    D. Russinoff. A Case Study in Formal Verification of Register-Transfer Logic: The Floating Point Adder of the AMD-K7TW Processor. In final preparation.Google Scholar
  50. 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. 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. 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. 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. 54.
    G. Steele, Jr. Common Lisp The Language, Second Edition. Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.zbMATHGoogle Scholar
  55. 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. 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. 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. 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. 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

Authors and Affiliations

  • Matt Kaufmann
    • 1
  1. 1.EDS CIO ServicesAustinUSA

Personalised recommendations