This book shows what can be done with computer aided reasoning. Included here are descriptions of mathematical, hardware, and software systems. These systems and their desired properties are modeled with formulas in a mathematical language. That language has an associated mechanized reasoning tool, called ACL2, which is used to prove that these properties hold. With these techniques it is possible to describe components clearly and reliably, permitting them to be combined in new ways with predictable results.
KeywordsModel Check Formal Method Chinese Remainder Theorem Hardware Description Language Common Lisp
Unable to display preview. Download preview PDF.