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. The results reported in
each case study, as ACL2 input scripts, as well as exercise
solutions for both books, are available from this page.
General
Is the information for this product incomplete, wrong or inappropriate?
Let us know about it.
Does this product have an incorrect or missing image?
Send us a new image.
Is this product missing categories?
Add more categories.
Review This Product
No reviews yet - be the first to create one!
Welcome to Loot.co.za!
Sign in / Register |Wishlists & Gift Vouchers |Help | Advanced search
