Synthesizing non-vacuous systems

Roderick Bloem; Hana Chockler; Masoud Ebrahimi; Ofer Strichman

doi:10.1007/978-3-319-52234-0_4

Synthesizing non-vacuous systems

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

^*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

10 Citations (Scopus)

239 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 language	English
Title of host publication	Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)
Subtitle of host publication	Lecture Notes in Computer Science
Publisher	Springer‐Verlag Berlin Heidelberg
Pages	55-72
Number of pages	18
Volume	10145
ISBN (Print)	9783319522333
DOIs	https://doi.org/10.1007/978-3-319-52234-0_4
Publication status	Published - 15 Jan 2017
Event	18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 - Paris, France Duration: 15 Jan 2017 → 17 Jan 2017

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	10145 LNCS
ISSN (Print)	03029743
ISSN (Electronic)	16113349

Conference

Conference	18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017
Country/Territory	France
City	Paris
Period	15/01/2017 → 17/01/2017

Access to Document

10.1007/978-3-319-52234-0_4

Synthesizing Non-Vacuous Systems_BLOEM_Publishedonline12January2017_GREEN AAMAccepted author manuscript, 434 KB

Cite this

Bloem, R., Chockler, H., Ebrahimi, M., & Strichman, O. (2017). Synthesizing non-vacuous systems. In Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science (Vol. 10145, pp. 55-72). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10145 LNCS). Springer‐Verlag Berlin Heidelberg. https://doi.org/10.1007/978-3-319-52234-0_4

Bloem, Roderick ; Chockler, Hana ; Ebrahimi, Masoud et al. / Synthesizing non-vacuous systems. Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science. Vol. 10145 Springer‐Verlag Berlin Heidelberg, 2017. pp. 55-72 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inbook{0c6793e4e2404451814d63b3fe6d3b5b,

title = "Synthesizing non-vacuous systems",

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.",

author = "Roderick Bloem and Hana Chockler and Masoud Ebrahimi and Ofer Strichman",

year = "2017",

month = jan,

day = "15",

doi = "10.1007/978-3-319-52234-0_4",

language = "English",

isbn = "9783319522333",

volume = "10145",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer‐Verlag Berlin Heidelberg",

pages = "55--72",

booktitle = "Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)",

note = "18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017 ; Conference date: 15-01-2017 Through 17-01-2017",

}

Bloem, R, Chockler, H, Ebrahimi, M & Strichman, O 2017, Synthesizing non-vacuous systems. in Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science. vol. 10145, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 10145 LNCS, Springer‐Verlag Berlin Heidelberg, pp. 55-72, 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017, Paris, France, 15/01/2017. https://doi.org/10.1007/978-3-319-52234-0_4

Synthesizing non-vacuous systems. / Bloem, Roderick; Chockler, Hana; Ebrahimi, Masoud et al.
Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science. Vol. 10145 Springer‐Verlag Berlin Heidelberg, 2017. p. 55-72 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 10145 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference paper › peer-review

TY - CHAP

T1 - Synthesizing non-vacuous systems

AU - Bloem, Roderick

AU - Chockler, Hana

AU - Ebrahimi, Masoud

AU - Strichman, Ofer

PY - 2017/1/15

Y1 - 2017/1/15

N2 - 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.

AB - 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.

U2 - 10.1007/978-3-319-52234-0_4

DO - 10.1007/978-3-319-52234-0_4

M3 - Conference paper

AN - SCOPUS:85010704963

SN - 9783319522333

VL - 10145

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 55

EP - 72

BT - Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI)

PB - Springer‐Verlag Berlin Heidelberg

T2 - 18th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2017

Y2 - 15 January 2017 through 17 January 2017

ER -

Bloem R, Chockler H, Ebrahimi M, Strichman O. Synthesizing non-vacuous systems. In Proceedings of 18th International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI): Lecture Notes in Computer Science. Vol. 10145. Springer‐Verlag Berlin Heidelberg. 2017. p. 55-72. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). Epub 2017 Jan 12. doi: 10.1007/978-3-319-52234-0_4

Synthesizing non-vacuous systems

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this