Library Services | Technical University of Kenya

Your cart is empty.
Normal view MARC view ISBD view

Scalable Techniques for Formal Verification [electronic resource] / by Sandip Ray.

By: Ray, Sandip [author.].
Contributor(s): SpringerLink (Online service).
Material type: materialTypeLabelBookPublisher: Boston, MA : Springer US : Imprint: Springer, 2010Description: XIV, 240p. online resource.Content type: text Media type: computer Carrier type: online resourceISBN: 9781441959980.Subject(s): Engineering | Computer aided design | Systems engineering | Engineering | Circuits and Systems | Computer-Aided Engineering (CAD, CAE) and DesignDDC classification: 621.3815 Online resources: Click here to access online
Contents:
Preliminaries -- Overview of Formal Verification -- to ACL2 -- Sequential Program Verification -- Sequential Programs -- Operational Semantics and Assertional Reasoning -- Connecting Different Proof Styles -- Verification of Reactive Systems -- Reactive Systems -- Verifying Concurrent Protocols Using Refinements -- Pipelined Machines -- Invariant Proving -- Invariant Proving -- Predicate Abstraction via Rewriting -- Formal Integration of Decision Procedures -- Integrating Deductive and Algorithmic Reasoning -- A Compositional Model Checking Procedure -- Connecting External Deduction Tools with ACL2 -- Conclusion -- Summary and Conclusion.
In: Springer eBooksSummary: 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.
Tags from this library: No tags from this library for this title. Log in to add tags.
No physical items for this record

Preliminaries -- Overview of Formal Verification -- to ACL2 -- Sequential Program Verification -- Sequential Programs -- Operational Semantics and Assertional Reasoning -- Connecting Different Proof Styles -- Verification of Reactive Systems -- Reactive Systems -- Verifying Concurrent Protocols Using Refinements -- Pipelined Machines -- Invariant Proving -- Invariant Proving -- Predicate Abstraction via Rewriting -- Formal Integration of Decision Procedures -- Integrating Deductive and Algorithmic Reasoning -- A Compositional Model Checking Procedure -- Connecting External Deduction Tools with ACL2 -- Conclusion -- Summary and Conclusion.

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.

There are no comments for this item.

Log in to your account to post a comment.

2017 | The Technical University of Kenya Library | +254(020) 2219929, 3341639, 3343672 | library@tukenya.ac.ke | Haile Selassie Avenue