Inhaltsangabe
Preliminaries.- Overview of Formal Verification.- to ACL2.- Sequential Program Verification.- Sequential Programs.- Operational Semantics and Assertional Reasoning.- Connecting Different Proof Styles.- Verification of Reactive Systems.- Reactive Systems.- Verifying Concurrent Protocols Using Refinements.- Pipelined Machines.- Invariant Proving.- Invariant Proving.- Predicate Abstraction via Rewriting.- Formal Integration of Decision Procedures.- Integrating Deductive and Algorithmic Reasoning.- A Compositional Model Checking Procedure.- Connecting External Deduction Tools with ACL2.- Conclusion.- Summary and Conclusion.
Die Inhaltsangabe kann sich auf eine andere Ausgabe dieses Titels beziehen.
