The Coq mailing list

[Dario Della Monica <dario.dellamonica AT uniud.it>]

*** apologies for cross-postings ***

===== Call for Attendance =====

-----------------------------------------------------------------------------
Third edition of the UniVr/UniUd Summer School on Formal Methods for
Cyber-Physical Systems - Udine, August 28-31

http://tcs.uniud.it/summer-school

+

Workshop on Synthesis, Monitoring and Learning - Udine, August 
31-September 1

http://tcs.uniud.it/smile

-----------------------------------------------------------------------------


Synthesis is a fundamental problem in computer science and mathematics, 
concerned with automatically generating programs that satisfy a given 
logical specification. Its applications span a range of domains, 
including model-based system design, software engineering, and automated 
theorem proving. For instance, designing a controller that guides the 
behavior of a reactive system, that is, a system that continually 
interacts with its environment, can be framed as a synthesis problem. 
Similarly, the design and verification of a distributed system often 
depend on distributed synthesis, which finds programs that enforce 
correct component interaction and satisfy desired specifications.

The third edition of the Summer School on Formal Methods for 
Cyber-Physical Systems offers an in-depth exploration of reactive 
synthesis, a topic that was already introduced in the first edition of 
the school. The lecturers will provide a systematic account of the main 
achievements and the current trends of research in reactive synthesis, 
covering both theory and applications.

The course will begin with an overview of the classical synthesis 
problem in the finite-state setting, as originally formulated by Church 
and solved by Buechi and Landweber. This introductory part will 
introduce the terminology of infinite two-player games, explain the 
automatic construction of winning strategies in “regular games”, and 
address history of the subject, discussing extensions and open problems. 
From there, the course will investigate approaches for making reactive 
synthesis more efficient and practical, including techniques for solving 
the synthesis problem in restricted settings, for decomposing the 
problem into subproblems, and for employing algorithms, data structures, 
and heuristics to manage complexity. Variants of the synthesis problem 
will also be explored, such as control strategies for hybrid and 
distributed systems, monitor synthesis, synthesis under incomplete 
information, distributed synthesis, and symmetric synthesis. The 
implementation of synthesis tools will also receive significant 
attention, with a focus on recent advances and applications of UPPAAL 
Stratego and the SYNTCOMP reactive synthesis competition.

The summer school will conclude with a workshop on emerging research 
trends in synthesis, monitoring, and learning, which showcases some 
exciting interactions between formal methods and machine learning. 
Distinguished invited speakers will lead the workshop. Participants will 
also have the opportunity to engage with peers from around the world and 
may propose to deliver short research talks voluntarily.


### Lecturers

Wolfgang Thomas - RWTH Aachen University, Germany

3-hour lecture on “Synthesis of strategies in infinite two-player games”

We give an introduction to the synthesis of reactive systems in the 
finite-state setting, using the terminology of infinite two-player games 
and explaining the automatic construction of winning strategies in 
“regular games”. We also address the history of the subject, discuss 
extensions, and mention basic problems that are still open.

Martin Zimmermann - Aalborg University, Denmark

3-hour lecture on “Synthesis of infinite-state systems”

The reactive synthesis problem asks to compute, from a given 
specification of the input-output behavior of a reactive system, a 
system satisfying this specification (or to determine that no such 
system exists). In this lecture, we consider the synthesis of 
infinite-state systems with a focus on pushdown systems, which model 
simple recursive systems with finite data. On a technical level, we show 
how to solve infinite games on configuration graphs of pushdown automata 
and present recent work on generalizations to history-deterministic 
pushdown automata.

Kim G. Larsen - Aalborg University, Denmark

3-hour lecture on “Synthesis and Optimization for Cyber Physical Systems”

In these lectures we will present recent advances and applications of 
the tool UPPAAL Stratego (www.uppaal.org) supporting automatic synthesis 
of guaranteed safe and near-optimal control strategies for Cyber 
Physical Systems (CPS). UPPAAL Stratego combines symbolic methods from 
model checking, reinforcement learning methods from machine learning, as 
well as abstraction techniques for hybrid games. Trade-offs between 
efficiency of strategy representation and degree of optimality subject 
to safety constraints will be discussed, as well as successful 
applications (autonomous driving maneuvers, heating systems and traffic 
control).

Dana Fisman - Ben Gurion University of the Negev, Israel

3-hour lecture on “Automata learning of languages of finite and infinite 
words”

In these lectures we will get acquainted with the research area called 
grammatical inference or automata learning.  We will start with the 
earliest results on the subject, and span different learning paradigms. 
We will describe several positive results, and efficient algorithms for 
learning regular languages. We will prove several negative results for 
learning different classes of languages in different learning paradigms. 
We will then discuss state-of-the-art results on learning regular 
languages of infinite words.

Swen Jacobs - CISPA Helmholtz-Center for Information Security, Germany

3-hour lecture on “Reactive synthesis: towards practice”

I will give an overview of different lines of research that try to make 
reactive synthesis (more) practical. This includes research into 
approaches to restrict the problem to more efficiently solvable 
fragments, into ways to split the problem into subproblems that can be 
solved independently or iteratively, and into efficient algorithms and 
data structures as well as heuristics that allow us to implement 
synthesis tools that can solve problems of significant size. I will 
report on progress observed in the reactive synthesis competition 
(SYNTCOMP), and on case studies and benchmark problems that demonstrate 
the capabilities of state-of-the-art synthesis tools.

Alessandro Cimatti - Fondazione Bruno Kessler, Italy

3-hour lecture on “Runtime verification and monitor synthesis”

Runtime Verification (RV) is a lightweight verification technique that 
aims at checking whether a run of a system under scrutiny (SUS) 
satisfies or violates a given correctness specification. The lecture 
will first overview the general framework of RV, and the techniques to 
synthesize run-time monitors that can be efficiently executed in 
combination with the SUS.  Then, we will cover the relationship between 
RV and the field of Fault Detection and Isolation (FDI). In FDI, runtime 
monitors are built taking into account models of the SUS, in order to 
monitor the occurrence of internal (faulty) conditions that are not 
directly observable.


### Programme

Monday, August 28

13:30 - 14:00 Registration
14:00 - 14:30 Course Introduction
14:30 - 16:00 Wolfgang Thomas
16:00 - 16:30 Coffee break
16:30 - 18:00 Wolfgang Thomas

Tuesday, August 29

09:30 - 11:00 Martin Zimmermann
11:00 - 11:30 Coffee break
11:30 - 13:00 Martin Zimmermann
13:00 - 14:00 Lunch
14:30 - 16:00 Kim G. Larsen
16:00 - 16:30 Coffee break
16:30 - 18:00 Kim G. Larsen

Wednesday, August 30

09:30 - 11:00 Dana Fisman
11:00 - 11:30 Coffee break
11:30 - 13:00 Dana Fisman
13:00 - 14:00 Lunch
14:30 - 16:00 Swen Jacobs
16:00 - 16:30 Coffee break
16:30 - 18:00 Swen Jacobs
19:00 - 23:00 Social dinner

Thursday, August 31

09:30 - 11:00 Alessandro Cimatti
11:00 - 11:30 Coffee break
11:30 - 13:00 Alessandro Cimatti
13:00 - 14:00 Lunch
14:30 - 16:30 Workshop on Synthesis, Monitoring and Learning

Friday, September 1

09:30 - 14:00 Workshop on Synthesis, Monitoring and Learning


### Admission and accommodation

The course is offered in a hybrid format giving the possibility to 
remotely attend the course (on the Microsoft Teams platform).

On-site places are limited and assigned on first come first served basis.

The registration fees are:
- On-site participation, 250.00 Euro + VAT 22%
- Online participation, 120.00 Euro + VAT 22%

Deadline for online application is August 18, 2023.
Participation application is available at 
https://www.cism.it/en/activities/courses/J2303/


### Contacts

CISM, Palazzo del Torso
Piazza Garibaldi 18, 39100 Udine, Italy
tel. +39 0432 248511
email: cism AT cism.it | www.cism.it


### Organization
Angelo Montanari - University of Udine, Italy
Gabriele Puppis - University of Udine, Italy
Tiziano Villa - University of Verona, Italy




--
Dario Della Monica, Associate Professor (Professore Associato)
Department of Mathematics, Computer Science, and Physics
University of Udine
via delle Scienze, 206 - 33100 Udine, Italy
cell: (+39) 328 2477327
email: dario.dellamonica [at] uniud.it
skype: dariodellamonica
web site: http://users.dimi.uniud.it/~dario.dellamonica/