Overview

This title 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 21 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. 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.

Full Product Details

Author:   Matt Kaufmann ,  Panagiotis Manolios ,  J Strother Moore
Publisher:   Springer
Imprint:   Springer
Edition:   2000 ed.
Volume:   4
Dimensions:   Width: 15.50cm , Height: 2.00cm , Length: 23.50cm
Weight:   1.510kg
ISBN:  

9780792378495

ISBN 10:   0792378490
Pages:   337
Publication Date:   30 June 2000
Audience:   College/higher education ,  Professional and scholarly ,  Undergraduate ,  Postgraduate, Research & Scholarly
Format:   Hardback
Publisher's Status:   Active
Availability:   In Print  
This item will be ordered in for you from one of our suppliers. Upon receipt, we will promptly dispatch it out to you. For in store availability, please contact us.

Table of Contents

1 Preface Introduction.- I Preliminaries.- 2 Overview.- 3 Summaries of the Case Studies.- 4 ACL2 Essentials.- II Case Studies.- 5 An Exercise in Graph Theory.- 6 Modular Proof: The Fundamental Theorem of Calculus.- 7 Mu-Calculus Model-Checking.- 8 High-Speed, Analyzable Simulators.- 9 Verification of a Simple Pipelined Machine Model.- 10 The DE Language.- 11 Using Macros to Mimic VHDL.- 12 Symbolic Trajectory Evaluation.- 13 RTL Verification: A Floating-Point Multiplier.- 14 Design Verification of a Safety-Critical Embedded Verifier.- 15 Compiler Verification Revisited.- 16 Ivy: A Preprocessor and Proof Checker for First-Order Logic.- 17 Knuth’s Generalization of McCarthy’s 91 Function.- 18 Continuity and Differentiability.

Reviews

Author Information

Tab Content 6

Author Website:  

Customer Reviews

Recent Reviews

No review item found!

Add your own review!

Countries Available

All regions