April 14 2015

Jump to: Tue | Wed | Thu
Session 1 - Viability

Chaired by Goran Frehse, University of Grenoble

10:30 - 11:00
A Viability Approach for Fast Recursive Feasible Finite Horizon Path Planning of Autonomous RC Cars
Alexander Liniger and John Lygeros
11:00 - 11:30
Reach-Avoid Problems with Time-Varying Dynamics, Targets and Constraints
Jaime Fisac, Mo Chen, Claire Tomlin and Shankar Sastry
11:30 - 12:00
An Improved Algorithm for Robust Safety Analysis of Sampled Data Systems
Ian M. Mitchell and Shahab Kaynama
Session 2 - Hybrid Automata

Chaired by Martin Fränzle, Carl von Ossietzky Universität Oldenburg

13:00 - 13:30
What's Decidable About Recursive Hybrid Automata?
Krishna S., Lakshmi Manasa and Ashutosh Trivedi
13:30 - 14:00
Bounded-Rate Multi-Mode Systems Based Motion Planning
Devendra Bhave, Sagar Jha, Krishna S., Sven Schewe and Ashutosh Trivedi
14:00 - 14:30
A sufficient condition for the boundedness of matrix products accepted by an automaton
Matthew Philippe and Raphaël Jungers
Session 3 - Abstraction

Chaired by Alexandre Donzé , UC Berkeley

15:00 - 15:30
Efficient Finite Abstraction of Mixed Monotone Systems
Samuel Coogan and Murat Arcak
15:30 - 16:00
Compositional Construction of Approximate Abstractions
Matthias Rungger and Majid Zamani
16:00 - 16:30
Computing Bisimulation Functions using SOS Optimization and delta-decidability over the Reals
Abhishek Murthy, Md. Ariful Islam, Radu Grosu and Scott Smolka
16:30 - 17:00
Probabilistic Diagnosability of Hybrid Systems
Yi Deng, Agung Julius and Alessandro D’innocenzo
Poster/Demo Session

Chaired by James Kapinski, Toyota Motors

17:00 - 20:00

Poster - Enforcing Temporal Logic Specifications via Reinforcement Learning
Austin Jones, Derya Aksaray, Zhaodan Kong, Mac Schwager and Calin Belta

Poster - Symbolic Control of Monotone Systems, Application to Ventilation Regulation in Buildings
Pierre-Jean Meyer, Antoine Girard and Emmanuel Witrant

Poster - A Stochastic Hybrid System Approach to Aggregated Load Modeling for Demand Response
Lin Zhao and Wei Zhang

Poster - Parallel State Space Exploration of Linear Systems with Inputs using XSpeed
Rajarshi Ray and Amit Gurung

Poster - Hybrid Representation of Rule-Based Systems
Matthew Clark and Kuldip Rattan

Poster - HyRG: A Random Generation Tool for Affine Hybrid Automata
Luan Nguyen, Sergiy Bogomolov, Christian Schilling and Taylor T Johnson

Poster - Stability and Stabilization of Polynomial Dynamical Systems using Bernstein Polynomials
Mohamed Amin Ben Sassi and Sriram Sankaranarayanan

Poster - Hybrid Multi-Contact Dynamics for Wedge Jumping Locomotion Behaviors
Ye Zhao, Donghyun Kim, Gray Thomas and Luis Sentis

Poster - Model-Based Design of Time-Triggered Real-time Embedded Systems for Digital Manufacturing
Jiang Wan, Arquimedes Canedo and Mohammad Al Faruque

Poster - Counterexample-Guided Stabilization of Switched Systems using Control Lyapunov Functions
Hadi Ravanbakhsh and Sriram Sankaranarayanan

Poster - Falsification of Safety Properties for Closed Loop Control Systems
Aditya Zutshi, Sriram Sankaranarayanan, Jyotirmoy Deshmukh, James Kapinski and Xiaoqing Jin

Demo - HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models
Stanley Bak, Sergiy Bogomolov and Taylor T Johnson

Demo - ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems
Fedor Shmarov and Paolo Zuliani

Demo - CyPhySim: A Cyber-Physical Systems Simulator
Christopher Brooks, Edward Lee, David Lorenzetti, Thierry Nouidui and Michael Wetter

Demo - Temporal-Difference Learning for Online Reachability Analysis
Anayo Akametalu and Claire Tomlin

Demo - Demonstration of Locomotion with the Powered Prosthesis AMPRO utilizing Online Optimization-Based Control
Huihua Zhao, Jacob Reher, Jonathan Horn, Victor Paredes and Aaron Ames

Demo - C2E2: A Tool For Verifying Annotated Hybrid Systems
Parasara Sridhar Duggirala, Matthew Potok, Sayan Mitra and Mahesh Viswanathan  

April 15, 2015

Jump to: Tue | Wed | Thu
Session 4 - Embedded and Networked Control

Chaired by Majid Zamani, Technical University of Munich

10:30 - 11:00
Dynamic Scheduling for Networked Control Systems
Indranil Saha, Sanjoy Baruah and Rupak Majumdar
11:00 - 11:30
Closed Loop Analysis of Control Command Software
Pierre Roux, Romain Jobredeaux and Pierre-Loic Garoche
11:30 - 12:00
Real-time Control under Clock Offsets between Sensors and Controllers
Kunihisa Okano, Masashi Wakaiki and Joao Hespanha
Keynote Address

Chaired by Antoine Girard, University of Grenoble

13:30 - 14:30
Will future cars have formally verified powertrain control software?
Jyotirmoy V. Deshmukh
Session 5 - Tools

Chaired by Antoine Girard, University of Grenoble

14:30 - 14:45
Tool Paper - HYST: A Source Transformation and Translation Tool for Hybrid Automaton Models
Stanley Bak, Sergiy Bogomolov and Taylor T Johnson
14:45 - 15:00
Tool Paper - ProbReach: Verified Probabilistic Delta-Reachability for Stochastic Hybrid Systems
Fedor Shmarov and Paolo Zuliani
Session 6 - Verification and Reachability Analysis

Chaired by Maria Prandini, Politecnico di Milano

15:30 - 16:00
On delta–sampling safety verification for discrete–time, possibly discontinuous systems
Ruxandra Valentina Bobiti and Mircea Lazar
16:00 - 16:30
Eliminating Spurious Transitions in Reachability with Support Functions
Goran Frehse, Sergiy Bogomolov, Marius Greitschus, Thomas Strump and Andreas Podelski
16:30 - 17:00
Finite State Approximation for Verification of Partially Observable Stochastic Hybrid Systems
Kendra Lesser and Meeko Oishi
17:00 - 17:30
Statistical Verification of Nonlinear Systems Using Set Oriented Methods
Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan and Geir Dullerud

April 16, 2015

Jump to: Tue | Wed | Thu
Session 7 - Specifications

Chaired by Ashuthosh Trivedi, IIT Bombay

10:30 - 11:00
Requirements for Hybrid Cosimulation Standards
David Broman, Lev Greenberg, Edward Lee, Michael Masin, Stavros Tripakis and Michael Wetter
11:00 - 11:30
SpaTeL: A Novel Spatial-Temporal Logic and Its Applications to Networked Systems
Iman Haghighi, Austin Jones, Zhaodan Kong, Ezio Bartocci, Radu Grosu and Calin Belta
11:30 - 12:00
Computing the Skorokhod Distance between Polygonal Traces
Rupak Majumdar and Vinayak Prabhu
Session 8 - Applications and Case Studies

Chaired by Pavithra Prabhakar, IMDEA Software Institute

13:30 - 14:00
First Steps toward Formal Controller Synthesis for Bipedal Robots
Aaron Ames, Paulo Tabuada, Bastian Schuermann, Wen-Loong Ma, Shishir Kolathaya, Matthias Rungger and Jessy Grizzle
14:00 - 14:30
Vulnerability analysis of dynamic power networks to stochastic link failure attacks
Sai Pushpak, Amit Diwadkar and Umesh Vaidya
14:30 - 14:45
Case Study - Towards Personalized Cancer Therapy Using Delta-Reachability Analysis
Bing Liu, Soonho Kong, Sicun Gao, Paolo Zuliani and Edmund Clarke
14:45 - 15:00
Case Study - Temporal Logic Motion Planning using POMDPs with Parity Objectives
Mária Svoreňová, Martin Chmelík, Kevin Leahy, Hasan Ferit Eniser, Krishnendu Chatterjee, Ivana Černá and Calin Belta
Session 9 - Synthesis

Chaired by Jyotirmoy Deshmukh, Toyota Motors

15:30 - 16:00
Reactive Synthesis from Signal Temporal Logic Specifications
Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray and Sanjit A. Seshia
16:00 - 16:30
Estimator-Based Reactive Synthesis under Incomplete Information
Rüdiger Ehlers and Ufuk Topcu
16:30 - 17:00
Temporal Logic Control for Stochastic Linear Systems using Abstraction Refinement of Probabilistic Games
Mária Svoreňová, Jan Křetínský, Martin Chmelík, Krishnendu Chatterjee, Ivana Cerna and Calin Belta
17:00 - 17:30
Cross-entropy Temporal Logic Motion Planning
Scott Livingston, Eric Wolff and Richard Murray