Computer-aided reasoning : ACL2 case studies

摘要: Preface. 1. Introduction. I: Preliminaries. 2. Overview. 3. Summaries of the Case Studies. 4. ACL2 Essentials. II: 5. An Exercise in Graph Theory J.S. Moore. 6. Modular Proof: The Fundamental Theorem Calculus M. Kaufmann. 7. Mu-Calculus Model-Checking P. Manolios. 8. High-Speed, Analyzable Simulators D. Greve, et al. 9. Verification a Simple Pipelined Machine Model J. Sawada. 10. DE Language. 11. Using Macros to Mimic VHDL Borrione, 12. Symbolic Trajectory Evaluation D.A. Jamsek. 13. RTL Verification: A Floating-Point Multiplier D.M. Russinoff, A. Flatau. 14. Design Safety-Critical Embedded Verifier Bertoli, Traverso. 15. Compiler Revisited W. Goerigk. 16. Ivy: Preprocessor and Proof Checker for First-Order Logic McCune, O. Shumsky. 17. Knuth's Generalization McCarthy's 91 Function Cowles. 18. Continuity Differentiability R. Gamboa. Bibliography. Index.