Anzeige
Erschienen in:
2006 | OriginalPaper | Buchkapitel
Why Waste a Perfectly Good Abstraction?
verfasst von : Arie Gurfinkel, Marsha Chechik
Erschienen in: Tools and Algorithms for the Construction and Analysis of Systems
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
Software model-checking based on the CEGAR framework can be made more precise by separating non-determinism from the lack of information due to abstraction. The two can be modeled individually using four-valued Belnap logic. In addition, this logic allows reasoning about negations effectively and thus enables checking of full CTL. In this paper, we present
Yasm
– a new symbolic software model-checker. Preliminary experience with
Yasm
shows that our implementation can effectively construct and analyze Belnap models without a substantial overhead when compared to its classical counterparts.