Synthesizing Non-Vacuous Systems

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Vacuity detection is a common practice accompanying model checking of hardware designs. Roughly speaking, a system satisfies a specification vacuously if it can satisfy a stronger specification obtained by replacing some of its subformulas with stronger expressions. If this happens then part of the specification is immaterial, which typically indicates that there is a problem in the model or the specification itself.
Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation
EditorsAhmed Bouajjani, David Monniaux
Place of PublicationCham
PublisherSpringer International Publishing AG
Pages55-72
Number of pages18
ISBN (Print)978-3-319-52234-0
Publication statusPublished - 2017

Fingerprint Dive into the research topics of 'Synthesizing Non-Vacuous Systems'. Together they form a unique fingerprint.

  • Projects

    Cite this

    Bloem, R., Chockler, H., Ebrahimi, M., & Strichman, O. (2017). Synthesizing Non-Vacuous Systems. In A. Bouajjani, & D. Monniaux (Eds.), Verification, Model Checking, and Abstract Interpretation (pp. 55-72). Cham: Springer International Publishing AG .