7:45-8:15

Registration

8:15-9:30 

Opening and Keynote Speaker

Rajeev Alur, University of Pennsylvania, USA

9:30-10:00

Coffee Break

10:00-12:00

Temporal logic applications

Chair: Sayan Mitra

10:00-10:30

A Decision Tree Approach to Data Classification using Signal Temporal Logic
Giuseppe Bombara, Cristian-Ioan Vasile, Francisco Penedo, Hirotoshi Yasuoka and Calin Belta

10:30-11:00

Temporal Logic as Filtering

Alena Rodionova, Ezio Bartocci, Dejan Nickovic and Radu Grosu 

11:00-11:30

Directed Specifications and Assumption Mining for Monotone Dynamical Systems

Eric S. Kim, Murat Arcak and Sanjit A. Seshia 

11:30-12:00

Diagnosis and Repair for Synthesis from Signal Temporal Logic Specifications
Shromona Ghosh, Dorsa Sadigh, Pierluigi Nuzzo, Vasumathi Raman, Alexandre Donzé, Alberto Sangiovanni-Vincentelli, Shankar Sastry and Sanjit Seshia 

12:00-13:30

Lunch

13:30-15:30

Analysis of switched systems

Chair: Maria Prandini

13:30-14:00

Computing the domain of attraction of switching systems subject to non-convex constraints
Nikolaos Athanasopoulos and Raphael Jungers

14:00-14:30

Generating unstable trajectories for Switched Systems via Dual Sum-Of-Squares techniques
Benoit Legat, Raphael Jungers and Pablo A. Parrilo 

14:30-15:00

A Topological Method for Finding Invariant Sets of Switched Systems
Laurent Fribourg, Eric Goubault, Sameh Mohamed and Sylvie Putot 

15:00-15:30

Hybridization for Stability Analysis of Switched Linear Systems

Pavithra Prabhakar and Miriam Garcia Soto 

15:30-16:00

Coffee Break

16:00-18:00

Case studies and tool papers

Chair: Akshay Rajhans

16:00-16:15

(Case study) Case Studies in Data-Driven Verification of Dynamical Systems
Alex Kozarev, John Quindlen, Jonathan How and Ufuk Topcu 

16:15-16:30

(Case study) Towards Model Checking of Implantable Cardioverter Defibrillators

Houssam Abbas, Kuk Jin Jang, Zhihao Jiang and Rahul Mangharam

16:30-16:40

(Tool paper) SL2SX Translator: From Simulink to SpaceEx Verification Tool
Stefano Minopoli and Goran Frehse 

16:40-16:50

(Tool paper) SCOTS: A Tool for the Synthesis of Symbolic Controllers

Matthias Rungger and Majid Zamani

16:50-18:00

Poster and demo presentations

Chair: Jim Kapinski

16:80-18:00

POSTERS:
* A Scalable Method for Finding Flaws in the Design of Technical Systems that Are Modelled by Ordinary Differential Equations, Jan Kuratko and Stefan Ratschan
* DynIBEX: a Differential Constraint Library for Studying Dynamical Systems, Julien Alexandre Dit Sandretto and Alexandre Chapoutot
* CSiSAT: A Satisfiability Solver for SMT Formulae with Continuous Probability Distributions, Yang Gao and Martin Franzle
* Temporal Logic Verification for Delay Differential Equations, Peter Nazier Mosaad and Martin Franzle
* Statistical Verification of the Toyota Powertrain Control Verification Benchmark, Nima Roohi, Yu Wang, Matthew West, Geir Dullerud and Mahesh Viswanathan
* Online Learning of STL Formulae for Signal Classification, Giuseppe Bombara and Calin Belta
DEMOS:
* Montre: A Tool for Monitoring Timed Regular Expressions, Dogan Ulus
* System Testing with S-TaLiRo: Recent Functionality and Additions, Bardh Hoxha, Adel Dokhanchi and Georgios Fainekos
* Hybrid Systems Model Transformations with HyST, Stanley Bak, Sergiy Bogomolov and Taylor T Johnson

18:00 - 20:00

CPS Community Forum

7:45-8:15

Registration

8:15-10:30 

Opening and Industrial Keynote Speakers

Ken Butts, Toyota, USA; Rada Rodriguez, Schneider Electric, Germany; Joe Salvo, GE Global Research, USA; Sabine Herlitschka, Infineon, Austria

10:30-11:00

Coffee Break

11:00-12:30

Safety and stability analysis

Chair: Taylor Johnson

11:00-11:30

Safety Analysis of Automotive Control Systems Using Multi-Modal Port-Hamiltonian Systems
Siyuan Dai and Xenofon Koutsoukos 

11:30-12:00

Verification and synthesis of timing contracts for embedded controllers
Mohammad Al Khatib, Antoine Girard and Thao Dang 

12:00-12:30

Formal Analysis of Robustness at Model and Code Level
Timothy Wang, Pierre-Loic Garoche, Pierre Roux, Romain Jobredeaux and Eric Feron 

12:30-14:00

Lunch

14:00-15:30

Methods for reachability analysis

Chair: Thao Dang

14:00-14:30

Symbolic-Numeric Reachability Analysis of Closed-Loop Control Software
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh and Xiaoqing Jin 

14:30-15:00

SMT-Based Analysis of Virtually Synchronous Distributed Hybrid Systems
Kyungmin Bae, Peter Olveczky, Soonho Kong and Sicun Gao 

15:00-15:30

Scalable Static Hybridization Methods for Analysis of Nonlinear Systems
Stanley Bak, Sergiy Bogomolov, Thomas Henzinger, Taylor T Johnson and Pradyot Prakash 

15:30-16:00

Coffee Break

16:00-18:00

Time- and event-based models

Chair: Necmiye Ozay

16:00-16:30

Adaptive Decentralized MAC for Event-triggered Networked Control Systems
Mikhail Vilgelm, Mohammadhossein Mamduhi, Wolfgang Kellerer and Sandra Hirche 

16:30-17:00

Event-separation properties and asymptotic behaviour of hybrid event-based control systems
Tobias Noesselt, Matthias Schultalbers and Jan Lunze 

17:00-17:30

Semi-autonomous Intersection Collision Avoidance through Job-shop Scheduling

Heejin Ahn and Domitilla Del Vecchio 

17:30-18:00

Building Power Consumption Models from Executable Timed I/O Automata Specifications

Benoit Barbot, Marta Kwiatkowska, Alexandru Mereacre and Nicola Paoletti

19:30-

Banquet, Concert, and Awards

7:45-8:15

Registration

8:15-9:30 

Opening and Keynote Speaker

Tomaso Poggio, CSAIL, MIT, USA

9:30-10:00

Coffee Break

10:00-12:00

Control synthesis

Chair: Majid Zamani

10:00-10:30

Control synthesis for large collections of systems with mode-counting constraints

Petter Nilsson and Necmiye Ozay 

10:30-11:00

Compositional Synthesis with Parametric Reactive Controllers
Rajeev Alur, Salar Moarref and Ufuk Topcu

11:00-11:30

Nonlinear Controller Synthesis and Automatic Workspace Partitioning for Reactive High-Level Behaviors
Jonathan Decastro and Hadas Kress-Gazit 

11:30-12:00

Robust Asymptotic Stabilization of Hybrid Systems using Control Lyapunov Functions
Ricardo Sanfelice 

12:00-13:30

Lunch

13:30-14:30

Invited speaker

Sandra Hirche, Optimal Co-Design of Scheduling and Control for Networked Systems

14:30-15:30

Models with uncertainty

Chair: Antoine Girard

14:30-15:00

Entropy and minimal data rates for state estimation and model detection
Daniel Liberzon and Sayan Mitra 

15:00-15:30

Safety Verification of Piecewise-Deterministic Markov Processes

Rafael Wisniewski, Christoffer Sloth, Manuela Bujorianu and Nir Piterman

15:30-16:00

Coffee Break

16:00-18:00

Reachability computation

Chair: Alex Donze

16:00-16:30

Computing Distances between Reach Flowpipes
Rupak Majumdar and Vinayak Prabhu 

16:30-17:00

Reachset Conformance Testing of Hybrid Automata

Hendrik Roehm, Jens Oehlerking, Matthias Woehrle and Matthias Althoff 

17:00-17:30

From Simulation Models to Hybrid Automata Using Urgency and Relaxation

Stefano Minopoli and Goran Frehse

17:30-18:00

Parallelotope Bundles for Polynomial Reachability

Tommaso Dreossi, Carla Piazza and Thao Dang