POPL 2017
Sun 15 - Sat 21 January 2017
Tue 17 Jan 2017 11:00 - 11:30 at Amphitheater 44 - Model Checking and Synthesis Chair(s): Ahmed Bouajjani

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.

Tue 17 Jan

10:30 - 12:00: VMCAI - Model Checking and Synthesis at Amphitheater 44
Chair(s): Ahmed Bouajjani
VMCAI-2017-papers148464540000010:30 - 11:00
VMCAI-2017-papers148464720000011:00 - 11:30
File Attached
VMCAI-2017-papers148464900000011:30 - 12:00