Scalable Techniques for Formal Verification

S. Ray

ISBN 978-4419-5997-3, 2010. Hardcover, 240 pages. Springer.

© Springer Science+Business Media, LLC 2010.


This book presents some state-of-the-art approaches in formal verification and methods to seamlessly integrate different formal verification techniques within a single logical foundation. It demonstrates methods for scaling up formal verification for large-scale computing systems using a combination of theorem proving and decision procedures. In particular, the book demonstrates how to develop customized, configurable reasoning tools (based on both theorem proving and decision procedures) for different verification domains, on top of a general-purpose purpose theorem prover. The customized reasoning tools discussed here extend theorem proving by significantly automating formal proofs on their target domains, but provide essentially the same soundness guarantees as the base theorem prover. The base theorem prover used here is ACL2, a state-of-the-art theorem prover which has been used to verify some of the largest industrial systems that have ever undergone formal verification.

The book should benefit researchers and practitioners looking to get a broad overview of the spectrum of formal verification techniques, as well as approaches for combining different techniques. The book discusses both theoretical and practical issues involved in integrating different reasoning methods to work in concert, and current approaches to their resolution.

In this book, we present

How to get the book