作者: Panagiotis Manolios , J. Strother Moore , Matt Kaufmann
DOI:
关键词:
摘要: From the Publisher: An Approach Computer-Aided Reasoning: An Approach is a textbook introduction to computer-aided reasoning. It can be used in graduate and upper-division undergraduate courses on software engineering or formal methods. also suitable conjunction with other books hardware design, discrete mathematics, theory, especially stressing formalism, rigor, mechanized support. appropriate for artificial intelligence automated reasoning as reference business industry. Current systems are often very complex trend towards increased complexity. Many of these critical importance; therefore making sure that they behave expected importance. By modeling computing mathematically, we obtain models prove correctly. The complexity makes such proofs long, complicated, error-prone. To further increase confidence our reasoning, use computer program check even automate some their construction. In this book present: A practical functional programming language closely related Common Lisp which define functions (which model systems) make assertions about defined functions; A logic correspond axioms; first-order, includes induction, allows us theorems system ACL2, language, logic, mechanical support proof process. The ACL2 hasbeen successfully applied projects commercial interest, including microprocessor, modeling, verification, microcode verification. This gives methodology formally those assistance. practicality demonstrated companion book, Computer-Aided Case Studies. Approximately 140 exercises distributed throughout book. Additional material freely available from home page Web, http://www.cs.utexas.edu/users/moore/ac12, solutions exercises, additional case studies research papers, detailed documentation. ACL2 Studies Computer-Aided Studies illustrates how productive innovative ways build, maintain systems. Included here technical papers written by twenty-one contributors report self-contained studies, sanitized industrial projects. deal wide variety ideas, floating-point arithmetic, microprocessor simulation, checking, symbolic trajectory evaluation, compilation, real analysis, several others. Computer-Aided meant two audiences: looking faster more reliably, wishing learn do this. former audience project managers students survey-oriented courses. latter professionals pursuing rigorous approaches Software Engineering, Formal Methods, Hardware Design, Theory Computation, Artificial Intelligence, Automated Reasoning. The divided into parts. Part I begins discussion effort involved using ACL2. contains brief its mechanization, intended give reader sufficient background read studies. thorough, may found Approach. heart II, where presented. contain whose Web. In addition, complete scripts necessary formalize all properties discussed For example, when say one formalizes multiplier proves it correct, mean not only you an English description was proved but entire content replay proofs, if wish, your copy ACL2. ACL2 obtained page, http://www.cs.utexas.edu/users/moore/ac12. results reported each study, input scripts, well exercise both books, page.