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. Provides a tutorial introduction to the state of the art in formal verification Unlike other books that focus on a particular techniques orapplication domains, this is the first authoritative reference to discuss disparate reasoning techniques and how they work with each other in solving different application problems Assumes no previous knowledge of formal reasoning and logic and includes numerous case studies to facilitate appreciation of the diversity of domains in which the techniques can be applied INDICE: Introduction.- Overview of Formal Verificaiton.- ACL2.- SequentialPrograms.- Analysis of Proof Strategies.- Using Theorem Proving for Verification Condition Generation.- Formalizing Reactive Programs.- Concurrent Programsas 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.
- ISBN: 978-1-4419-5997-3
- Editorial: Springer
- Encuadernacion: Cartoné
- Páginas: 340
- Fecha Publicación: 01/06/2010
- Nº Volúmenes: 1
- Idioma: Inglés