The list of accepted papers is availabe here.

Prof. Edward A. Lee
University of California at Berkeley, USA
Prof. Sriram Sankaranarayanan
University of Colorado Boulder, USA
Prof. Mingsheng Ying
University of Technology Sydney, Australia and Tsinghua University, China

All talks are given in the Institute of Software, Chinese Academy of Science, Building 5, room 334 (3rd floor) Lecture Hall, 4th floor. See the Conference venue page for details on how to reach the Institute.

The booklet of the SETTA conference is available to be downloaded.

November 8 – Tuesday
14:30–17:00 Registration
November 9 – Wednesday
08:00–17:00 Registration
08:30–09:00 Welcome ceremony (chair: Deepak Kapur)
09:00–10:10 Invited talk by Prof. Edward A. Lee (chair: Deepak Kapur)
10:10–10:45 Tea break
10:45–12:05 Session: Concurrency (chair: Lijun Zhang)
10:45–11:15 Xiaoju Dong, Yuxi Fu and Daniele Varacca: Place Bisimulation and Liveness for Open Petri Nets
11:15–11:45 Qingguo Xu, Robert De Simone and Julien Deantoni: Divergence Detection for CCSL Specification via Clock Causality Chain
11:45–12:05 Joost-Pieter Katoen, Hao Wu and Xiaoxiao Yang: Performance Evaluation on Modern Concurrent Data Structures (short paper)
12:15–14:00 Lunch
14:00–15:30 Session: Probabilistic systems I (chair: Andrea Turrini)
14:00–14:30 Andrzej Mizera, Jun Pang and Qixia Yuan: GPU-accelerated Steady-state Computation of Large Probabilistic Boolean Networks
14:30–15:00 Yuxin Deng, Wenjie Du and Daniel Gebler: Behavioural Pseudometrics for Nondeterministic Probabilistic Systems
15:00–15:30 Ernst Moritz Hahn and Arnd Hartmanns: A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques
15:30–16:00 Tea break
16:00–17:20 Session: Program verification (chair: Sriram Sankaranarayanan)
16:00–16:30 Tianhai Liu, Shmuel Tyszberowicz, Mihai Herda, Bernhard Beckert, Daniel Grahl and Mana Taghdiri: Computing Specification-Sensitive Abstractions for Program Verification
16:30–17:00 Tatsuya Abe, Tomoharu Ugawa, Toshiyuki Maeda and Kousuke Matsumoto: Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models
17:00–17:20 Ruifang Zhao, Ke Liu, Hongli Yang and Zongyan Qiu: Identifying XML Schema Constraints Using Temporal Logic (short paper)
18:00–19:30 Reception
November 10 – Thursday
08:30–11:30 Registration
09:00–10:10 Invited talk by Prof. Sriram Sankaranarayanan (chair: Naijun Zhan)
10:10–10:45 Tea break
10:45–11:45 Session: Real-time systems (chair: Sanjoy Baruah)
10:45–11:15 Bingbing Fang, Guoqiang Li, Daniel Sun and Hongming Cai: Schedulability Analysis of Timed Regular Tasks by Under-Approximation on WCET
11:15–11:45 Kim Guldstrand Larsen, Axel Legay, Marius Mikuńćionis, Cyrille Jegourel, Danny Bøgsted Poulsen and Sean Sedwards: Importance Sampling for Stochastic Timed Automata
11:45–13:00 Lunch
13:00–18:00 Excursion
18:30–22:00 Banquet
November 11 – Friday
08:30–17:00 Registration
09:00–10:10 Invited talk by Prof. Mingsheng Ying (chair: Joost-Pieter Katoen)
10:10–10:45 Tea break
10:45–12:15 Session: Program logic (chair: Xinyu Feng)
10:45–11:15 Zhilin Wu: Semipositivity in Separation Logic with Two Variables
11:15–11:45 Søren Enevoldsen, Jiri Srba, Kim Guldstrand Larsen and Andreas Dalsgaard: Distributed Computation of Fixed Points on Dependency Graphs
11:45–12:15 Mikkel Hansen, Kim Guldstrand Larsen, Radu Mardare, Mathias Ruggaard Pedersen and Bingtian Xue: A Complete Approximation Theory for Weighted Transition Systems
12:15–14:00 Lunch
14:00–15:30 Session: Verification (chair: Fei He)
14:00–14:30 Jacopo Mauro, Gereon Kremer, Erika Abraham, Florian Corzilius and Einar Broch Johnsen: Zephyrus2: On the Fly Deployment Optimization using SMT and CP Technologies
14:30–15:00 Qiang Wang: Exploiting Symmetry for Efficient Verification of Infinite-State Component-based Systems
15:00–15:30 Waqar Ahmed and Osman Hasan: Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach
15:30–16:00 Tea break
16:00–17:20 Session: Probabilistic systems II (chair: David Jansen)
16:00–16:30 Yong Li, Wanwei Liu, Andrea Turrini, Ernst Moritz Hahn and Lijun Zhang: An Efficient Synthesis Algorithm for Parametric Markov Chains against Linear Time Properties
16:30–17:00 Ratul Saha, Madhavan Mukund and Jagadeesh Chandra Bose R P,: Time-bounded Statistical Analysis of Resource-constrained Business Processes with Distributed Probabilistic Systems
17:00–17:20 Debasmita Lohar, Anudeep Dunaboyina, Dibyendu Das and Soumyajit Dey: Failure Estimation of Behavioral Specifications (short paper)
17:20–17:30 Closing ceremony (chair: Deepak Kapur and Naijun Zhan)
18:30–21:30 PC Dinner

Prof. Edward A. Lee: Dependable Cyber-Physical Systems

Cyber-physical systems are integrations of computation, communication networks, and physical dynamics. Applications include manufacturing, transportation, energy production and distribution, biomedical, smart buildings, and military systems, to name a few. Increasingly, today, such systems leverage Internet technology, despite a significant mismatch in technical objectives. A major challenge today is to make this technology reliable, predictable, and controllable enough for "important" things, such as safety-critical and mission-critical systems. In this talk, I will analyze how emerging technologies can translate into better models and better engineering methods for this evolving Internet of Important things.

Prof. Sriram Sankaranarayanan: From finitely many simulations to flowpipes

Flowpipe construction techniques generalize symbolic execution for continuous-time models by computing future trajectories for sets of inputs and initial states. In doing so, they capture infinitely many behaviors of the underlying system, thus promising exhaustive verification. We examine the progress in this area starting from techniques for linear systems to recent progress in reasoning about nonlinear dynamical systems. We demonstrate how this area of research transforms fundamental results from dynamical systems theory into useful computational techniques for reasoning about cyber-physical systems. This progress has led to increasingly popular tools for verifying cyber-physical systems with applications to important verification problems for medical devices and automotive software. We demonstrate how recent approaches have exploited commonly encountered properties of the underlying continuous models such as monotonicity, incremental stability and structural dependencies to verify properties for larger and more complex systems. Despite this progress, many challenges remain. We present some of the key theoretical and practical challenges that need to be met before flowpipe construction can be a true "technology" for verifying industrial-scale systems.

Prof. Mingsheng Ying: Toward Automatic Verification of Quantum Programs

Programming is error-prone. Programming a quantum computer and designing quantum communication protocols are even worse due to the weird nature of quantum systems. Therefore, verification techniques for quantum programs and quantum protocols will be indispensable whence commercial quantum computers and quantum communication systems are available. In the last 10 years, various verification techniques for classical programs including program logics and model-checking have been extended to deal with quantum programs. This talk summaries several results obtained by the author and his collaborators in this line of research.