Write a Blog >>
VMCAI 2017
Sun 15 - Tue 17 January 2017
co-located with POPL 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

Displayed 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
30m
Talk
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
30m
Talk
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
30m
Talk
Solving Nonlinear Integer Arithmetic with MCSat
VMCAI
Dejan Jovanović SRI International