Synthesizing Non-Vacuous Systems

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Research output: Chapter in Book/Report/Conference proceedingConference paperpeer-review


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
Number of pages18
ISBN (Print)978-3-319-52234-0
Publication statusPublished - 2017


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

Cite this