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.
slides (masoud_vmcai_slides.pdf) | 820KiB |
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
10:30 - 12:00 | Model Checking and SynthesisVMCAI at Amphitheater 44 Chair(s): Ahmed Bouajjani IRIF, Université Paris Diderot | ||
10:30 30mTalk | Reachability for dynamic parametric processes VMCAI Anca Muscholl Université de Bordeaux / LaBRI, Helmut Seidl Technische Universität München, Igor Walukiewicz CNRS, LaBRI | ||
11:00 30mTalk | Synthesizing Non-Vacuous Systems VMCAI Roderick Bloem Institute of Software Technology, Graz University of Technology , Hana Chockler , ma e , Ofer Strichman Technion File Attached | ||
11:30 30mTalk | Solving Nonlinear Integer Arithmetic with MCSat VMCAI Dejan Jovanović SRI International |