Scalable Techniques for Formal Verification

This book is about formal veri?cation, that is, the use of mathematical reasoning to ensure correct execution of computing systems. With the increasing use of c- puting systems in safety-critical and security-critical applications, it is becoming increasingly important for our well-being to ensure t...

Szczegółowa specyfikacja

Zapisane w:
Opis bibliograficzny
1. autor: Ray, Sandip. (Autor, http://id.loc.gov/vocabulary/relators/aut)
Korporacja: SpringerLink (Online service)
Format: Elektroniczne E-book
Język:English
Wydane: New York, NY : Springer US : Imprint: Springer, 2010.
Wydanie:1st ed. 2010.
Hasła przedmiotowe:
Dostęp online:https://doi.org/10.1007/978-1-4419-5998-0
Etykiety: Dodaj etykietę
Nie ma etykietki, Dołącz pierwszą etykiete!
Spis treści:
  • 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.