SRI Logo
About Us|R and D Divisions|Careers|Newsroom|Contact Us|SRI Home
  SRI Logo

Abstract and Model Check while you Prove
 by Dr. Hassen Sa´di & Dr. Natarajan Shankar.

Lecture Notes in Computer Science, Number 1633.
From Computer-Aided Verification (CAV'99).
Edited by Nicolas Halbwachs and Doron Peled.
Springer-Verlag, Trento, Italy.
July, 1999.
Pages 443–454.

The construction of abstractions is essential for reducing large or infinite state systems to small or finite state systems. Boolean abstractions, where boolean variables replace concrete predicates, are an important class that subsume several abstraction schemes. We show how boolean abstractions can be constructed simply, efficiently, and precisely for infinite state systems while preserving properties in the full mu-calculus. We also propose an automatic refinement algorithm which refines the abstraction until the property is verified or a counterexample is found. Our algorithm is implemented as a proof rule in the PVS verification system. With the abstraction proof rule, proof strategies combining deductive proof construction, model checking, and abstraction can be defined entirely within the PVS framework.
BibTEX Entry
    AUTHOR = {Hassen Sa\"{i}di and Natarajan Shankar},
    TITLE = {Abstract and Model Check while you Prove},
    BOOKTITLE = {Computer-Aided Verification (CAV'99)},
    YEAR = {1999},
    EDITOR = {Nicolas Halbwachs and Doron Peled},
    SERIES = {Lecture Notes in Computer Science},
    NUMBER = {1633},
    PAGES = {443--454},
    ADDRESS = {Trento, Italy},
    MONTH = {jul},
    PUBLISHER = {Springer-Verlag},
    URL = {}


About Us  |  R&D Divisions  |  Careers  |  Newsroom  |  Contact Us
© 2024 SRI International 333 Ravenswood Avenue, Menlo Park, CA 94025-3493
SRI International is an independent, nonprofit corporation. Privacy policy