Computer-Aided Reasoning

by Kaufmann, Matt; Manolios, Panagiotis; Moore, J Strother

• ISBN13: 9780792378495
• ISBN10: 0792378490
• Format: Hardcover
• Copyright: 2000-06-01
• Publisher: Kluwer Academic Pub

Summary

Computer-Aided Reasoning: ACL2 Case Studies illustrates how the computer-aided reasoning system ACL2 can be used in productive and innovative ways to design, build, and maintain hardware and software systems. Included here are technical papers written by twenty-one contributors that report on self-contained case studies, some of which are sanitized industrial projects. The papers deal with a wide variety of ideas, including floating-point arithmetic, microprocessor simulation, model checking, symbolic trajectory evaluation, compilation, proof checking, real analysis, and several others. Computer-Aided Reasoning: ACL2 Case Studies is meant for two audiences: those looking for innovative ways to design, build, and maintain hardware and software systems faster and more reliably, and those wishing to learn how to do this. The former audience includes project managers and students in survey-oriented courses. The latter audience includes students and professionals pursuing rigorous approaches to hardware and software engineering or formal methods. Computer-Aided Reasoning: ACL2 Case Studies can be used in graduate and upper-division undergraduate courses on Software Engineering, Formal Methods, Hardware Design, Theory of Computation, Artificial Intelligence, and Automated Reasoning. The book is divided into two parts. Part I begins with a discussion of the effort involved in using ACL2. It also contains a brief introduction to the ACL2 logic and its mechanization, which is intended to give the reader sufficient background to read the case studies. A more thorough, textbook introduction to ACL2 may be found in the companion book, Computer-Aided Reasoning: An Approach. The heart of the book is Part II, where the case studies are presented. The case studies contain exercises whose solutions are on the Web. In addition, the complete ACL2 scripts necessary to formalize the models and prove all the properties discussed are on the Web. For example, when we say that one of the case studies formalizes a floating-point multiplier and proves it correct, we mean that not only can you read an English description of the model and how it was proved correct, but you can obtain the entire formal content of the project and replay the proofs, if you wish, with your copy of ACL2. ACL2 may be obtained from its home page, http://www.cs.utexas.edu/users/moore/acl2. The results reported in each case study, as ACL2 input scripts, as well as exercise solutions for both books, are available from this page.

Table of Contents

Preface	xi
Introduction	1	(6)
I Preliminaries	7	(32)
Overview	9	(12)
Some Questions	9	(1)
Some Answers	10	(2)
Anecdotal Evidence from Two Projects	12	(3)
Sociology	15	(2)
Toy Models	17	(1)
Requirements on the User	18	(3)
Summaries of the Case Studies	21	(6)
ACL2 Essentials	27	(12)
Data Types	27	(1)
Expressions	28	(4)
Events	32	(5)
Concluding Remarks	37	(2)
II Case Studies	39	(278)
An Exercise in Graph Theory	41	(34)
J Strother Moore
Getting Started	43	(1)
The Primitives of Directed Graphs	44	(2)
The Specification of Find-Path	46	(2)
The Definitions of Find-Path and Find-Next-Step	48	(3)
Sketch of the Proof of Our Main Theorem	51
Observation 0	52	(54)
Observation 1	54	(3)
Observation 2	57	(9)
Observation 3	66	(1)
The Main Theorem	67	(1)
The Specification of Find-Path	67	(1)
Reflexive Definitions	68	(2)
Less Elementary Further Work	70	(1)
General Lessons	71	(4)
Modular Proof: The Fundamental Theorem of Calculus	75	(18)
Matt Kaufmann
A Modular Proof Methodology	76	(4)
Case Study: The Fundamental Theorem of Calculus	80	(8)
Conclusion	88	(5)
Appendix: The Depth-3 Outline for FTOC	89	(4)
Mu-Calculus Model-Checking	93	(20)
Panagiotis Manolios
Set Theory	95	(5)
Fixpoint Theory	100	(2)
Relation Theory	102	(1)
Models	103	(1)
Mu-Calculus Syntax	103	(2)
Mu-Calculus Semantics	105	(4)
Temporal Logic	109	(2)
Conclusions	111	(2)
High-Speed, Analyzable Simulators	113	(24)
David Greve
Matthew Wilding
David Hardin
High-Speed Simulators	114	(11)
TINY : A High-Speed Simulator Example	125	(1)
Simulator Execution Analysis	126	(9)
Conclusion	135	(2)
Verification of a Simple Pipelined Machine Model	137	(14)
Jun Sawada
A Three-Stage Pipelined Machine and Its Correctness	137	(5)
Intermediate Abstraction and Invariant	142	(5)
Proving the Commutative Diagram	147	(2)
Related Work	149	(2)
The DE Language	151	(16)
Warren A. Hunt, Jr.
DE Language Example	152	(1)
Recognizing the DE Language	153	(7)
The DE Simulator	160	(4)
An Example DE Simulator Call	164	(1)
An Example DE Proof	164	(1)
Challenges for the Reader	165	(1)
Conclusion	166	(1)
Using Macros to Mimic VHDL	167	(18)
Dominique Borrione
Philippe Georgelin
Vanderlei Rodrigues
The VHDL Subset	168	(3)
The Semantic Model	171	(4)
Elaboration of the Model	175	(2)
Symbolic Simulation	177	(2)
Proof of the Circuit	179	(3)
Conclusion	182	(3)
Symbolic Trajectory Evaluation	185	(16)
Damir A. Jamsek
Booleans and Uncertainty	186	(3)
Nodes, States, and Runs	189	(1)
Expressions, Circuits, and Trajectories	190	(2)
Assertions and Theorems	192	(5)
STE Inference Rules	197	(2)
Deductive Proofs	199	(2)
RTL Verification: A Floating-Point Multiplier	201	(32)
David M. Russinoff
Arthur Flatau
A Library of Floating-Point Arithmetic	202	(7)
The RTL Language	209	(7)
Correctness of the Multiplier	216	(17)
Design Verification of a Safety-Critical Embedded Verifier	233	(14)
Piergiorgio Bertoli
Paolo Traverso
Formalization of the Industrial Problem	233	(7)
Proof of Correct Design	240	(4)
Conclusions	244	(1)
Exercises	245	(2)
Compiler Verification Revisited	247	(18)
Wolfgang Goerigk
A Proved Correct Compiler	249	(6)
The Compiler Bootstrap Test	255	(2)
Self-Reproducing Programs	257	(2)
The Incorrect Executable	259	(3)
Conclusions	262	(3)
Ivy: A Preprocessor and Proof Checker for First-Order Logic	265	(18)
Walliam McCune
Olga Shumsky
Basic Definitions	267	(5)
The Proof Procedure	272	(6)
Disproving Conjectures	278	(1)
Infinite Domains	279	(1)
Completeness	280	(1)
Exercises	281	(2)
Knuth's Generalization of McCarthy's 91 Function	283	(18)
John Cowles
McCarthy's 91 Function	285	(2)
Knuth's Generalization	287	(1)
Using ACL2 to Meet Knuth's Challenge	288	(13)
Continuity and Differentiability	301	(16)
Ruben Gamboa
Non-Standard Analysis	302	(2)
Continuity	304	(4)
Differentiability	308	(7)
Conclusions	315	(2)
Bibliography	317	(8)
Index	325