Scalable Techniques for Formal Verification - Ray, Sandip; SpringerLink (Online service) (New York, NY : Springer US : Imprint: Springer, 2010)
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.
Keywords: Electronic circuits; Computer-aided engineering; Circuits and Systems; Computer-Aided Engineering (CAD, CAE) and Design