Synthesizing non-vacuous systems

Roderick Bloem, Hana Chockler, Masoud Ebrahimi, Ofer Strichman*

*Corresponding author for this work

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

9 Citations (Scopus)
206 Downloads (Pure)

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. We propose to apply the concept of vacuity to the synthesis problem. In synthesis, there is often a problem that the specifications are incomplete, hence under-specifying the desired behaviour, which may lead to a situation in which the synthesised system is different than the one intended by the designer. To address this problem we suggest an algorithm and a tool for non-vacuous bounded synthesis. It combines synthesis for universal and existential properties; the latter stems from the requirement to have at least one interesting witness for each strengthening of the specification. Even when the system satisfies the specification non-vacuously, our tool is capable of improving it by synthesizing a system that has additional interesting witnesses. The user decides when the system reflects their intent.

Original languageEnglish
Title of host publicationProceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
Subtitle of host publicationLecture Notes in Computer Science
PublisherSpringer‐Verlag Berlin Heidelberg
Pages55-72
Number of pages18
Volume10145
ISBN (Print)9783319522333
DOIs
Publication statusPublished - 15 Jan 2017
Event18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 - Paris, France
Duration: 15 Jan 201717 Jan 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10145 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Conference

Conference18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
Country/TerritoryFrance
CityParis
Period15/01/201717/01/2017

Fingerprint

Dive into the research topics of 'Synthesizing non-vacuous systems'. Together they form a unique fingerprint.

Cite this