Scalable Techniques for Formal Verification /
| Main Author: | |
|---|---|
| Corporate Author: | |
| Format: | eBook |
| Language: | English |
| Published: |
New York, NY :
Springer US : Imprint: Springer,
2010.
|
| Edition: | 1st ed. 2010. |
| Subjects: |
Table of Contents:
- 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.