SynCoP 2026
11th International Workshop on Synthesis of Complex Parameters
Torino, Sunday 12th April 2026
About
SynCoP (11th 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). Parameterised verification is the task of verifying the correctness of this kind of systems regardless the number of their components.
SynCoP 2026 is an event associated to ETAPS 2026.
Important dates
Abstract submission deadline: 4th March 2026
Author notification: 6th March 2026
Workshop: Sunday 12th April 2026
Keynote speakers
Nathalie Bertrand
Inria Rennes 🇫🇷
- Reduction theorems for effective parameterized verification of round-based distributed algorithms
Abstract: Standard formal methods techniques apply to the verification of
distributed algorithms only for a fixed number of finite-state processes.
Parameterized verification aims at generalizing this to checking correctness for
any number of processes, but typically assumes each process is finite-state. We
address a more general setting, asynchronous round-based distributed algorithms,
in which every process executes an unbounded sequence of asynchronous rounds and
is therefore infinite-state. The resulting systems are unbounded in two
dimensions: the number of processes and the number of rounds.
Towards efficient verification of parameterized round-based distributed
algorithms, we exhibit a series of reduction theorems, that collapses the
unbounded round dimension into a single counter and reduces the parameterized
verification problem to LTL model checking of a counter system. This enables the
use of off-the-shelf state-of-the-art infinite-state model checkers such as
NuXmv. We demonstrate the feasibility of our approach by verifying several
round-based consensus and leader election algorithms.
This is a joint work with Pranav Ghorpade and Sasha Rubin.
Sebastian Junges
Radboud University in Nijmegen 🇳🇱
- How Satisfiability-Modulo-Probabilistic-Model-Checking Finds Robust and Concise Policies
Abstract: This talk connects the synthesis of decision tree representations of MDP policies as a complex parameter synthesis problem.
It illustrates the specific problem, reformulates it in more abstract terms, and then solves it using parameter synthesis techniques.
In the talk, we focus on the novel satisfiability-modulo-probablistic-model-checking framework, that effectively yet flexibly tackle different variations of this problem.
The work builds work previously presented at CAV’25 and AAAI’26.
Rajarshi Roy
University of Liverpool 🏴
- Synthesizing Temporal Logic Specifications via Learning from Examples
Abstract: Almost all formal verification methods require one to precisely specify the requirements a system is expected to satisfy. In practice, these requirements must be expressed in formal specification languages, a task that is often difficult. This process can be time-consuming and prone to human error, as it demands substantial expertise to capture complex system behavior. To tackle the challenge of formalizing specifications, in this talk, I explore a data-driven approach in which temporal logic specifications are automatically learned from examples of system behavior. I will discuss how this learning-based approach must be adapted to reflect practical settings: data is frequently noisy, negative examples may be unavailable, and observations may involve uncertainties. Moreover, different temporal logic specification languages suit different scenarios: Linear Temporal Logic (LTL) operates over discrete traces, Metric Temporal Logic (MTL) over continuous signals, and Computation Tree Logic (CTL) over branching models. I will present symbolic learning algorithms for these different scenarios and discuss the types of guarantees that can be provided. I will also provide a perspective on how specification learning can be integrated with modern AI systems going forward.
Jeremy Sproston
Università degli Studi di Torino 🇮🇹
- Probabilistic Timed Automata with Clock-Dependent Probabilities
Abstract: Probabilistic timed automata are classical timed automata extended with discrete probability distributions over edges, and have been employed in the modelling and analysis of numerous case studies in which the interplay of time and probabilistic choice is integral to the system description. This talk focuses on clock-dependent probabilistic timed automata, which generalise probabilistic timed automata by allowing the probabilities of discrete transitions to be described by piecewise continuous functions on clock variables, allowing the modelling of a direct relationship between time passage and the likelihood of system events. We consider the problem of deciding whether the maximum probability of reaching a certain state set is above a threshold in a clock-dependent probabilistic timed automaton. While this problem is undecidable for clock-dependent probabilistic timed automata with at least three clock variables, the problem is decidable for restricted classes of clock-dependent probabilistic timed automata with one clock, via transformations to interval Markov chains and parametric Markov chains.
Organizers
Rémi Parrot
École Centrale Nantes 🇫🇷
B Srivathsan
Chennai Mathematical Institute 🇮🇳
Steering committee
Étienne André
Nantes Université 🇫🇷
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 2026 seeks short abstracts only. Recently published works, ongoing works, or works under submission are welcome.
The non-strict page limit is 3 pages (excluding bibliography) single column. All accepted abstracts will be made available to the participants of SynCoP 2026, but they will not result in referenced publications.
Authors of accepted abstracts will be invited to give an informal presentation during the workshop.
Submission will be made in English in PDF format via a simple email at: syncop2026@lipn13.fr
Submission deadline: 4th March 2026
Acceptance notification: 6th March 2026
Program
Sunday morning (room TBA)
☕️ Coffee and registration
08:30-08:55
👨🏫 Opening
08:55-09:00
Keynote speaker: TBA
09:00-09:50
- TBA
☕️ Coffee break
09:50-10:30
Technical session
10:30-11:00
- TBA
- TBA
11:00-11:30
- TBA
- TBA
11:30-12:00
- TBA
- TBA
🥙 Lunch break
Sunday afternoon (room TBA)
Invited speaker: TBA
13:30-14:20
- TBA
☕️ Coffee break
14:20-14:40
Invited speaker: TBA
14:40-15:55
- TBA
☕️ Coffee break
15:55-16:15
🥙 Workshop dinner (TBA)
Pictures of the event
To come after the event!
Former editions
SynCoP 2025
10th edition
Aarhus 🇩🇰
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
ITS Torino, Via Jacopo Durandi 10, Torino, Italy
Display large map
Email Us
syncop2026@lipn13.fr