Scalable Techniques for Formal Verification
S. Ray
ISBN 978-4419-5997-3, 2010. Hardcover, 240 pages. Springer.
© Springer Science+Business Media, LLC 2010.
Description
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
- a tutorial introduction to the state of the art in formal
verification;
- techniques for making disparate reasoning techniques work with
each other in solving different verification problems;
- a compositional approach for applying assertional
reasoning on operationally modeled sequential programs;
- a formalization of a notion of stuttering trace containment and
its application on reactive system verification;
- an extendible, deductive procedure to compute predicate
abstractions that can be implemented effectively in a theorem prover
to compute system invariants; and
- techniques for combining theorem proving and model checking, and
associated logical and engineering challenges.
How to get the book