ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic

SynCoP aims at bringing together researchers working on verification and parameter synthesis for systems with discrete or continuous parameters, in which the parameters influence the behaviour of the system in ways that are complex and difficult to predict. Such problems may arise for real-time, hybrid or probabilistic systems in a large variety of application domains. The parameters can be continuous (e.g. timing, probabilities, costs) or discrete (e.g. number of processes). The goal can be to identify suitable parameters to achieve desired behaviour, or to verify the behaviour for a given range of parameter values.

Systems composed of a finite but possibly arbitrary number of identical components occur everywhere from hardware design (e.g. cache coherence protocols) to distributed applications (e.g. client-server applications). Parameterised verification is the task of verifying the correctness of this kind of systems regardless the number of their components.

Call for Papers

In addition to invited presentations, SynCoP 2019 organises a call for papers. SynCoP seeks short abstracts only. Recently published works, ongoing works, or works under submission are welcome. The page limit is 3 pages (excluding bibliography), LNCS style. All accepted abstracts will be made available to the participants of SynCoP 2019 but they will not result in referenced publications. Authors of accepted abstracts will be required to give a presentation during the workshop. We intend to select the best abstracts and presentations for a full paper in a special issue of a journal.

Submissions must be made in English in PDF format through Easychair.

See the call for papers for further details.

Past editions

You're viewing the program in a time zone which is different from your device's time zone change time zone

Sat 6 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

11:00 - 12:00
Timed systemsSynCoP at S10
On Parameterised Jobshop Scheduling Problems
13:30 - 15:30
ApplicationsSynCoP at S10
Parametric statistical model checking of UAV flightplan
Fault-tolerant matrix factorisation: a formal model and proof
Camille Coti LIPN, Université Paris 13, Laure Petrucci Université Paris 13, Daniel Alberto Torres Gonzalez LIPN, Université Paris 13

Sun 7 Apr

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

09:00 - 10:30
Parameter synthesis for LTLSynCoP at S10
Parameter Synthesis for Timed Automata with Clock-Aware LTL Properties
Pruning NDFS for Parametric Timed Automata
Laure Petrucci Université Paris 13, Jaco van de Pol Aarhus University

The scientific subject of the workshop covers (but is not limited to) the following areas:

  • parameter synthesis,

  • parametric model checking,

  • regular model checking,

  • robustness analysis,

  • parameterised logics, decidability and complexity issues,

  • formalisms such as parametric timed and hybrid automata, parametric time(d) Petri nets, parametric probabilistic (timed) automata, parametric Markov Decision Processes, networks of identical processes,

  • specifications in automata and logic, term and graph rewriting, Petri nets, process algebra, …

  • validation methods via assertional and regular model checking, reachability and coverability decision procedures, abstractions, theorem proving, constraint solving, …

  • interactions between discrete and continuous parameters,

  • tools and applications to hardware design, cache coherence protocols, security and communication protocols, multithreaded and concurrent programs, programs with relaxed memory models, mobile and distributed systems, database languages and systems, biological systems, …