Anzeige
Erschienen in:
2008 | OriginalPaper | Buchkapitel
Approximate Invariant Property Checking Using Term-Height Reduction for a Subset of First-Order Logic
verfasst von : Hiroaki Shimizu, Kiyoharu Hamaguchi, Toshinobu Kashiwabara
Erschienen in: Automated Technology for Verification and Analysis
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
In order to verify larger and more complicated systems with model checking, it is necessary to apply some abstraction techniques. Using a subset of first-order logic, called EUF, is one of them. The EUF model checking problem is, however, generally undecidable. In this paper, we introduce a technique called term-height reduction, to guarantee the termination of state enumeration in EUF model checking. This technique generates an over-approximate set of states including all the reachable states. By checking a designated invariant property, we can guarantee whether the invariant property always holds for the design, when verification succeeds. We apply our algorithm to a simple C program and a DSP design and show the experimental results.