SynCoP 2025
10th International Workshop on Synthesis of Complex Parameters
Aarhus, Monday 25 August 2025
About
SynCoP (10th International Workshop on Synthesis of Complex Parameters) 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). Parametrised verification is the task of verifying the correctness of this kind of systems regardless the number of their components.
SynCoP 2025 is an event associated to CONFEST 2025.
Important dates
Abstract submission deadline: 30 June 7th July 2025
Author notification: 7 July 14th July 2025
Final version of abstracts: 28th July 2025
Workshop: Monday 25th August 2025
Keynote speaker
Orna Kupferman
Hebrew University of Jerusalem
- Synthesis of Privacy-Preserving Systems
Abstract: The talk describes a framework for automatic synthesis that addresses the privacy of the system and its environment. In addition to a specification, the user of the synthesis algorithm provides a list of secrets. Both the specification and the secrets describe on-going behaviors, given by LTL formulas. We distinguish between two settings. In the first, values of some input and output signals are hidden from an observer in a way that respects budget constraints on the set of signals that may be hidden. In all environments, the specification should be satisfied and the value of the secrets should be hidden from the observer. In the second setting, the system and the environment hide values of some signals from each other. Here, in all environments, the specification should be satisfied despite the incomplete information, and the satisfaction value of the secrets should be hidden.
Joint work with Ofer Leshkowitz and Naama Shamash-Halevy
Invited speakers
B Srivathsan
Chennai Mathematical Institute 🇮🇳
- Canonical synthesis of one-clock deterministic timed automata
Abstract: Minimization and learning algorithms for DFAs are built on the elegant idea of canonical synthesis: the Myhill–Nerode theorem tells us exactly how to construct the unique minimal DFA for any regular language. Extending this principle to timed automata, however, introduces new challenges — most notably, how to canonically synthesize the placement of clock resets and timing constraints on transitions. We address this question for the subclass of one-clock deterministic timed automata (1-DTAs).
In this talk, we present a theory of canonical synthesis for 1-DTAs, grounded in a Myhill–Nerode-style theorem. Our key insight is to view these automata through the lens of half-integral words — timed words where every delay is either an integer or an integer plus 0.5 — and to associate with them a canonical reset function. This characterization forms the basis for new minimization procedures and active learning algorithms that are provably guaranteed to synthesize the canonical 1-DTA.
Joint work with Kyveli Doveri and Pierre Ganty
Martin Zimmermann
Aalborg University 🇩🇰
- Monitoring Real-Time Systems Under Parametric Delay
Abstract: This talk describes a framework for monitoring real-time systems against specifications given by timed Büchi automata. Classically, this task is achieved by symbolic execution of automata on the trace observed from the system. This direct construction however only is faithful if observation of the trace is immediate in the sense that the monitor can assign exact time stamps to the actions it observes, which is rarely true in practice due to the substantial and fluctuating parametric delays introduced by the circuitry connecting the observed system to its monitoring device. We present a purely zone-based online monitoring algorithm, which handles such parametric delays exactly without recurrence to costly verification procedures for parametric timed automata.
Joint work with Martin Fränzle, Thomas M. Grosen, and Kim G. Larsen.
Organizers
Étienne André
Université Sorbonne Paris Nord 🇫🇷
Swen Jacobs
CISPA Helmholtz Center for Information Security, Saarbrücken 🇩🇪
Steering committee
Étienne André
Université Sorbonne Paris Nord 🇫🇷
Benoit Delahaye
Nantes Université 🇫🇷
Giorgio Delzanno
Università degli Studi di Genova 🇮🇹
Peter Habermehl
University Paris Cité 🇫🇷
Kim Guldstrand Larsen
Aalborg University 🇩🇰
Engel Lefaucheux
Loria, Inria 🇫🇷
Didier Lime
École Centrale de Nantes 🇫🇷
Wojciech Penczek
IPI-PAN 🇵🇱
Laure Petrucci
Université Sorbonne Paris Nord 🇫🇷
Call for informal presentations
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, …
SynCoP 2025 seeks short abstracts only. Recently published works, ongoing works, or works under submission are welcome.
The page limit is 3 pages (excluding bibliography) single column. All accepted abstracts will be made available to the participants of SynCoP 2025 but they will not result in referenced publications.
Authors of accepted abstracts will be required to give an informal presentation during the workshop.
Submission will be made in English in PDF format with a simple email at: syncop25@lipn13.fr
Submission deadline: 30 June 2025 7th July 2025
Acceptance notification: 7th July 2025 14th July 2025
Program
Monday morning (Room M2.3 (1420-228))
☕️ Coffee and registration
08:30-08:55
👨🏫 Opening
08:55-09:00
Keynote speaker: Orna Kupferman
09:00-09:50
- Synthesis of Privacy-Preserving Systems
☕️ Coffee break
09:50-10:30
Technical session
10:30-11:00
- Formal Model Predictive Control Using Dynamic Bayesian Network Approximations
- Yahia Bahloul, Benoît Barbot, Adrien Le Coënt and Nihal Pekergin
11:00-11:30
- Efficient synthesis algorithms for Parametric Timed Games with merging
- Mikael Bisgaard Dahlsen-Jensen, Baptiste Fievet, Laure Petrucci, and Jaco van de Pol
11:30-12:00
- Probabilistic Abstraction and Verification of Nonlinear Hybrid Dynamical Systems
- David Julien, Gilles Ardourel, Guillaume Cantin, and Benoît Delahaye
🥙 Lunch break
Monday afternoon (Room M2.3 (1420-228))
Invited speaker: B Srivathsan
13:30-14:20
- Canonical synthesis of one-clock deterministic timed automata
☕️ Coffee break
14:20-14:40
☕️ Coffee break
15:55-16:15
🥙 Workshop dinner
Pictures of the event
To come after the event!
Former editions
SynCoP 2024
9th edition
Lëtzebuerg 🇱🇺
SynCoP 2023
8th edition
Paris 🇫🇷
SynCoP 2022
7th edition
München 🇩🇪
SynCoP 2019
6th edition
Praha 🇨🇿
SynCoP 2018
5th edition
Θεσσαλονίκη 🇬🇷
SynCoP + PV 2017
4th edition
Uppsala 🇸🇪
SynCoP 2016
3rd edition
Eindhoven 🇳🇱
SynCoP 2015
2nd edition
London 🏴
SynCoP 2014
1st edition
Grenoble 🇫🇷
See the generic SynCoP page.
Contact
Contact us
Location
Room M2.3 (1420-228), The Conference Center, Aarhus University, Fredrik Nielsens Vej 2-4, 8000 Aarhus C, Denmark
Email Us
syncop25@lipn13.fr
Display large map