Tue 17 Jan 2017 10:30 - 11:00 at Amphitheater 44 - Model Checking and Synthesis Chair(s): Ahmed Bouajjani
In a dynamic parametric process every sub-process may spawn arbitrarily many, identical child processes, that may communicate either over global variables, or over local variables that are shared with their parent.
We show that reachability for dynamic parametric processes is decidable under mild assumptions. These assumptions are e.g. met if individual processes are realized by pushdown systems, or even higher-order pushdown systems. We also provide algorithms for subclasses of pushdown dynamic parametric processes, with complexity ranging between NP and DEXPTIME.
Tue 17 JanDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
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 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 |