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 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00
|Reachability for dynamic parametric processes|
|Synthesizing Non-Vacuous Systems|
Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , Masoud Ebrahimi Institute of Applied Information Processing and Communications, Graz University of Technology, Ofer Strichman TechnionFile Attached
|Solving Nonlinear Integer Arithmetic with MCSat|
Dejan Jovanović SRI International