- Full Description
This book presents state-of-the-art approaches to formal verification techniques to seamlessly integrate different formal verification methods within a single logical foundation. It should benefit researchers and practitioners looking to get a broad overview of the spectrum of formal verification techniques, as well as approaches to combining such techniques within a single framework. Coverage includes a range of case studies showing how such combination is fruitful in developing a scalable verification methodology for industrial designs. This book outlines both theoretical and practical issues involved in integrating different reasoning methods to work in concert, and current approaches to their resolution.
- Table of Contents
Table of Contents
- Overview of Formal Verificaiton.
- Sequential Programs.
- Analysis of Proof Strategies.
- Using Theorem Proving for Verification Condition Generation.
- Formalizing Reactive Programs.
- Concurrent Programs as a Reactive System.
- Rewriting and Abstract Interpretation.
- Integrating Deductive and Algorithmic Reasoning.
- A Formally Verified Compositional Model Checking Procedure.
- Integrating Arbitrary Decision Procedures with Theorem Proving.
Please Login to submit errata.No errata are currently published