About

The School on Formal Methods for Cyber-Physical Systems addresses the foundations, techniques, and tools for analysis, verification, control, synthesis, implementation, and applications of cyber-physical systems (CPS). Applications mainly deal with engineering and natural systems, including signal circuits, robotics, automotive and avionics, large-scale infrastructure networks, as well as biochemical and physiological processes. 

This second edition of the school has the goal of presenting the state of the art of the current techniques in reachability analysis for hybrid systems, using either a numerical or symbolic approach, to enable doctoral students and young researchers to advance the field and apply the developed methodologies to concrete scenarios promoting their application in the industrial practice. Within the school this year we will also hold a workshop that covers the same topics. The workshop is more technical in nature and it is aimed at researchers interested in the most recent developments in the field. Workshop presentations will be distributed along the five days of the school.

The scope of the school includes, but is not restricted to, the following topics:

- Reachability analysis approaches for hybrid systems

- Flow-pipe construction

- State set representations and operations

- Trajectory generation from symbolic paths; counterexample computation

- Abstraction techniques for hybrid systems

- Reliable integration

- Stochastic/probabilistic hybrid systems

- Logics to reason about hybrid systems

- Domain-specific approaches in biology, robotics, etc.

- Tools, benchmarks, and case studies

The school is supported by grants from the PhD School in Natural Sciences and Engineering and the Department of Computer Science of the University of Verona.



When

From 03/06/2019 to 07/06/2019
add to your calendar

Where

Dipartimento di Informatica
Strada le Grazie 15, Verona (Italy)
view accommodation info
show on Google Maps /

By plane

The airport of Verona is connected to the main European and national cities. From the airport you can reach the city by taxi or by bus. A shuttle bus connects the airport to Verona Porta Nuova train station.

By Train

The train station of Verona Porta Nuova is connected with all the main Italian cities by fast and local trains. For the train schedule, please check the Italian railway company. From the station you can reach the Department of Computer Science by bus or by taxi.

By bus

Bus line 21 (towards S. Giovanni Lupatoto) get off at the first bus stop after Borgo Roma hospital; from the bus stop, you can see the department’s buildings. You can also catch bus line 22 (towards Policlinico/San Giovanni Lupatoto) and line 93 (during the night and on Sundays), towards Cadidavid. For these last two bus lines, get off at Borgo Roma hospital, then follow the map below. You can find timetables and line maps at the ATV website.

By car
Take the A4 Milano-Venezia highway, exit Verona Sud then follow the direction "Ospedale Borgo Roma" (hospital), on the right. At the hospital, go straight, cross the small bridge on a river and take the second right. From here you can see the department buildings on your left.


Important locations for the School

All lectures of the School will be held in Sala Verde (also called Aula Verde or Verde Hall in English), which is in the pyramid building between the Department of Computer Science and the Department of Biotechnology. The right-most building, and the first that you will encounter from the car access, is the Biotechnology Department. When inside the Department, just keep the left for the pyramid. There will be directions affixed at the entrances and corridors of the ground floor for both buildings. Coffee breaks will be held very close to the entrance of Sala Verde, on its left towards the Computer Science Department. Lunches will be in the open space at the entrance of the Computer Science Department. The laboratory session on Thursday afternoon will be at the Laboratorio Ciberfisico (Cyber-physical Systems Laboratory) in the Computer Science Department, first floor, left wing. For all breaks, lunches and the laboratory you will be accompanied by the organizers. Finally, for the social event, see http://cps.di.univr.it/social-events?school_edition=2019 .


The registrations are closed.


Tarsie in Santa Maria in Organo, Verona
Tarsia of Santa Maria in Organo church in Verona

Lecturers

Schedule


TimeSpeakerTitle

09:15–09:30

Tiziano Villa Welcome

09:30–11:00

Tiziano Villa Introduction to Hybrid Systems Verification

11:00–11:20

Coffee Break

11:20–12:20

Luca Geretti Numerical Aspects in Reachability Analysis of Nonlinear Hybrid Systems

12:20–13:20

Erika Abraham Reachability Analysis Techniques for Hybrid Systems

13:20–14:20

Lunch

14:20–16:20

Erika Abraham Reachability Analysis Techniques for Hybrid Systems

16:20–16:40

Coffee Break

16:40–17:30

Erika Abraham Workshop: What is going on in HyPro?

TimeSpeakerTitle

09:00–11:00

Alessandro Abate Automated Verification and Synthesis of CPS Models

11:00–11:20

Coffee Break

11:20–13:20

Carla Piazza Reachability Computation and Parameter Synthesis through Bernstein Coefficients

13:20–14:20

Lunch

14:20–15:10

Alessandro Abate Workshop: Verification and Learning of CPS: Model-Based and Data-Driven Methods

15:10–15:30

Coffee Break

15:30–16:00

Alessandro Abate Automated Verification and Synthesis of CPS Models: Software Demonstration

TimeSpeakerTitle

09:00–11:00

Luca Benvenuti An Overview of Dynamical Systems. Models for Hybrid Systems

11:00–11:20

Coffee Break

11:20–12:20

Luca Benvenuti Hybrid Systems in Automotive Electronics Design: Engine and Power Train Hybrid Model

12:20–13:20

Alessandro Cimatti SMT-Based Verification of Hybrid Systems

13:20–14:20

Lunch

14:20–15:20

Alessandro Cimatti SMT-Based Verification of Hybrid Systems

15:20–15:40

Coffee Break

15:40–16:30

Leonardo Mangeruca Workshop: Challenges on the Application of Formal Methods for Validation and Verification in Aerospace Systems Engineering

20:00–23:00

Social Dinner

TimeSpeakerTitle

10:10–11:00

Alessandro Abate Workshop: Certified Learning with Logic Guidance

11:00–11:20

Coffee Break

11:20–12:20

Matthias Althoff Online Verification of Cyber-Physical Systems

12:20–13:10

Alessandro Cimatti Workshop: SMT-Based Analysis of Switching Multi-Domain Linear Kirchhoff Networks

13:20–14:20

Lunch

14:20–16:20

Matthias Althoff Laboratory: Building Your Own Reachability Analyzer with CORA

16:20–16:40

Coffee Break

16:40–17:30

Luca Geretti Workshop: Differential Inclusions for Decomposition of Continuous and Hybrid Systems

TimeSpeakerTitle

09:00–11:00

Goran Frehse From Numerical to Set-Based Analysis of Hybrid Systems

11:00–11:20

Coffee Break

11:20–12:20

Goran Frehse Workshop: Counterexample-Guided Refinement of Template Reachability

12:20–12:25

Tiziano Villa Farewell

Social Events

Scientific Committee

Luca Geretti, Dipartimento di Informatica, Università di Verona, Italy
Tiziano Villa, Dipartimento di Informatica, Università di Verona, Italy
Paolo Fiorini, Dipartimento di Informatica, Università di Verona, Italy
Riccardo Muradore, Dipartimento di Informatica, Università di Verona, Italy

Organizers

Luca Geretti, Dipartimento di Informatica, Università di Verona, Italy (luca.geretti@univr.it)
Tiziano Villa
, Dipartimento di Informatica, Università di Verona, Italy (tiziano.villa@univr.it)
Marta Capiluppi, Dipartimento di Informatica, Università di Verona, Italy (marta.capiluppi@univr.it)