Symposium on Dependable Software Engineering
Theories, Tools and Applications
Beijing, China, Nov. 9-11, 2016
The list of accepted papers is availabe here.
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|
|November 9 – Wednesday|
|08:30–09:00||Welcome ceremony (chair: Deepak Kapur)|
|09:00–10:10||Invited talk by Prof. Edward A. Lee (chair: Deepak Kapur)|
|10:45–12:05||Session: Concurrency (chair: Lijun Zhang)|
|10:45–11:15||Place Bisimulation and Liveness for Open Petri Nets:|
|11:15–11:45||Divergence Detection for CCSL Specification via Clock Causality Chain:|
|11:45–12:05||Performance Evaluation on Modern Concurrent Data Structures (short paper):|
|14:00–15:30||Session: Probabilistic systems I (chair: Andrea Turrini)|
|14:00–14:30||GPU-accelerated Steady-state Computation of Large Probabilistic Boolean Networks:|
|14:30–15:00||Behavioural Pseudometrics for Nondeterministic Probabilistic Systems:|
|15:00–15:30||A Comparison of Time- and Reward-Bounded Probabilistic Model Checking Techniques:|
|16:00–17:20||Session: Program verification (chair: Sriram Sankaranarayanan)|
|16:00–16:30||Computing Specification-Sensitive Abstractions for Program Verification:|
|16:30–17:00||Reducing State Explosion for Software Model Checking with Relaxed Memory Consistency Models:|
|17:00–17:20||Identifying XML Schema Constraints Using Temporal Logic (short paper):|
|November 10 – Thursday|
|09:00–10:10||Invited talk by Prof. Sriram Sankaranarayanan (chair: Naijun Zhan)|
|10:45–11:45||Session: Real-time systems (chair: Sanjoy Baruah)|
|10:45–11:15||Schedulability Analysis of Timed Regular Tasks by Under-Approximation on WCET:|
|11:15–11:45||Importance Sampling for Stochastic Timed Automata:|
|November 11 – Friday|
|09:00–10:10||Invited talk by Prof. Mingsheng Ying (chair: Joost-Pieter Katoen)|
|10:45–12:15||Session: Program logic (chair: Xinyu Feng)|
|10:45–11:15||Semipositivity in Separation Logic with Two Variables:|
|11:15–11:45||Distributed Computation of Fixed Points on Dependency Graphs:|
|11:45–12:15||A Complete Approximation Theory for Weighted Transition Systems:|
|14:00–15:30||Session: Verification (chair: Fei He)|
|14:00–14:30||Zephyrus2: On the Fly Deployment Optimization using SMT and CP Technologies:|
|14:30–15:00||Exploiting Symmetry for Efficient Verification of Infinite-State Component-based Systems:|
|15:00–15:30||Formalization of Fault Trees in Higher-order Logic: A Deep Embedding Approach:|
|16:00–17:20||Session: Probabilistic systems II (chair: David Jansen)|
|16:00–16:30||An Efficient Synthesis Algorithm for Parametric Markov Chains against Linear Time Properties:|
|16:30–17:00||Time-bounded Statistical Analysis of Resource-constrained Business Processes with Distributed Probabilistic Systems:|
|17:00–17:20||Failure Estimation of Behavioral Specifications (short paper):|
|17:20–17:30||Closing ceremony (chair: Deepak Kapur and Naijun Zhan)|
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.