Synthesizing Non-Vacuous Systems

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem Konferenzband

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.
Originalspracheenglisch
TitelVerification, Model Checking, and Abstract Interpretation
Redakteure/-innenAhmed Bouajjani, David Monniaux
ErscheinungsortCham
Herausgeber (Verlag)Springer International Publishing AG
Seiten55-72
Seitenumfang18
ISBN (Print)978-3-319-52234-0
PublikationsstatusVeröffentlicht - 2017

Fingerprint Untersuchen Sie die Forschungsthemen von „Synthesizing Non-Vacuous Systems“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren