Scalable Techniques for Formal Verification

1. Introduction
Sandip Ray

2. Overview of Formal Verification
Sandip Ray

3. Introduction to ACL2
Sandip Ray

4. Sequential Programs
Sandip Ray

5. Operational Semantics and Assertional Reasoning
Sandip Ray

6. Connecting Different Proof Styles
Sandip Ray

7. Reactive Systems
Sandip Ray

8. Verifying Concurrent Protocols Using Refinements
Sandip Ray

9. Pipelined Machines
Sandip Ray

10. Invariant Proving
Sandip Ray

11. Predicate Abstraction via Rewriting
Sandip Ray

12. Integrating Deductive and Algorithmic Reasoning
Sandip Ray

13. A Compositional Model Checking Procedure
Sandip Ray

14. Connecting External Deduction Tools with ACL2
Sandip Ray

15. Summary and Conclusion
Sandip Ray

Avainsanat: Engineering, Circuits and Systems, Computer-Aided Engineering (CAD, CAE) and Design