Regular Papers (submission ordered)

On the Polytope Escape Problem for Linear Dynamical Systems
Joel Ouaknine, Joao Sousa Pinto, and James Worrell

Towards Optimal State Estimation of Switched Nonlinear Systems with finite-data-rate measurements
Hussein Sibai and Sayan Mitra

Convex Interpolation Control with Formal Guarantees for Disturbed and Constrained Nonlinear Systems
Bastian Schurmann and Matthias Althoff

Invariance Feedback Entropy of Non-deterministic Control Systems
Matthias Rungger and Majid Zamani

Sound and Automated Synthesis of Digital Stabilizing Controllers for Continuous Plants
Alessandro Abate, Iury Bessa, Dario Cattaruzza, Lucas Cordeiro, Cristina David, Pascal Kesseli, and Daniel Kroening

A Small Gain Theorem for Parametric Assume-Guarantee Contracts
Eric Kim, Murat Arcak, and Sanjit A. Seshia

Structural Analysis of Multi-Mode DAE Systems
Albert Benveniste, Benoit Caillaud, Hilding Elmqvist, Khalil Ghorbal, Martin Otter, and Marc Pouzet

Piecewise–differentiable trajectory outcomes in mechanical systems subject to unilateral constraints
Andrew M. Pace and Samuel A. Burden

On a class of maximal invariance inducing control strategies for large collections of switched systems
Petter Nilsson and Necmiye Ozay

Forward inner-approximated reachability of non-linear continuous systems
Eric Goubault and Sylvie Putot

Reachability Computation for Switching Diffusions: Finite Abstractions of Continuous Models
Luca Laurenti, Alessandro Abate, Luca Bortolussi, Marta Kwiatkowska, Luca Cardelli, and Milan Ceska

Relaxed decidability and the robust semantics of Metric Temporal Logic
Houssam Abbas, Matthew O'Kelly, and Rahul Mangharam

Safety Verification of Nonlinear Hybrid Systems Based on Invariant Clusters
Hui Kong, Sergiy Bogomolov, Christian Schilling, Yu Jiang and Thomas Henzinger

Dynamic Periodic Event-Triggered Control for Linear Systemsa>
D.P. Borgers, V.S. Dolk, and W.P.M.H. Heemels

Scheduling of embedded controllers under timing contracts
Mohammad Al Khatib, Antoine Girard, and Thao Dang

Path-Complete Graphs and Common Lyapunov Functions
David Angeli, Matthew Philippe, Nikolaos Athanasopoulos, and Raphaël Jungers

Forward stochastic reachability analysis for uncontrolled linear systems using Fourier transforms
Abraham Vinod, Baisravan Homchaudhuri, and Meeko Oishi

SMC: Satisfiability modulo Convex Optimization
Yasser Shoukry, Pierluigi Nuzzo, Alberto L. Sangiovanni-Vincentelli, Sanjit A. Seshia, George J. Pappas, and Paulo Tabuada

Sampling-based approximate optimal control under temporal logic constraints
Jie Fu, Ivan Papusha, and Ufuk Topcu

Robust Model Checking of Timed Automata under Clock Drifts
Nima Roohi, Pavithra Prabhakar, and Mahesh Viswanathan

Formal Synthesis of Stabilizing Controllers for Switched Systems
Pavithra Prabhakar and Miriam García Soto

Bipedal Robotic Running with DURUS-2D: Bridging the Gap between Theory and Experiment
Wenlong Ma, Shishir Kolathaya, Eric Ambrose, Christian Hubicki, and Aaron Ames

Coupling Policy Iterations with Piecewise Quadratic Lyapunov Functions
Assale Adje

Robust Abstractions for Control Synthesis: Robustness Equals Realizability for Linear-Time Properties
Jun Liu

Controller Synthesis for Reward Collecting Markov Processes in Continuous Space
Sadegh Soudjani and Rupak Majumdar

Tools and Case Studies

Statistical Verification of the Toyota Powertrain Control Verification Benchmark
Nima Roohi, Yu Wang, Matthew West, Geir Dullerud, and Mahesh Viswanathan

HyLAA: A Tool for Computing Simulation-Equivalent Reachability for Linear Systems
Stanley Bak and Parasara Sridhar Duggirala

Sapo: A Tool for the Reachability Computation and Parameter Synthesis of Polynomial Dynamical Systems
Tommaso Dreossi

Abnormal Data Classification Using Time-Frequency Temporal Logic
Luan Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy Deshmukh, Ken Butts, and Taylor Johnson

Contact