SETTA 2017
Symposium on Dependable Software Engineering
Theories, Tools and Applications
Changsha, China, Oct. 23-25, 2017
CONFERENCE PROGRAM
Day 1: 23 October 2017 | |
---|---|
08:00–08:30 | Registration |
08:30–09:00 | Welcome by Program Chairs |
09:00–10:00 | Keynote 1 (Chair: Oleg Sokolsky) Cliff Jones, Newcastle University General Lessons from a Rely/Guarantee Development |
10:00–10:30 | Tea break |
10:30–12:00 | Session 1 - Probabilistic and statistical analysis (Chair: Lijun Zhang) |
10:30–11:00 | Polynomial-Time Alternating Probabilistic Bisimulation for Interval MDPs | :
11:00–11:30 | Better Automated Importance Splitting for Transient Rare Events | :
11:30–12:00 | On the Criticality of Probabilistic Worst-Case Execution Time Models | :
12:15–13:45 | Lunch |
14:00–15:30 | Session 2 – Timed and hybrid systems (Chair: Xiaoguang Mao) |
14:00–14:30 | Nested Timed Automata with Invariants | :
14:30–15:00 | Multi-core cyclic executives for safety-critical systems | :
15:00–15:30 | Compositional Hoare-style Reasoning about Hybrid CSP in the Duration Calculus | :
15:30–16:00 | Tea break |
16:00–17:30 | Session 3 – Program analysis (Chair: Stefano Schivo) |
16:00–16:30 | Termination of Semi-Algebraic Loop Programs | :
16:30–17:00 | Computing Exact Loop Bounds for Bounded Program Verification | :
17:00–17:30 | AndroidLeaker: A Hybrid Checker for Collusive Leak in Android Applications | :
18:00–19:30 | Reception |
Day 2:24 October 2017 | |
08:00– 09:00 | Registration |
09:00–10:00 |
Keynote 2 (Chair: Naijun Zhan) Rupak Majumdar, Max Planck Institute for Software Systems Formal Methods for Building a Multi-Robot Task Server |
10:00–10:30 | Tea break |
10:30–12:00 | Session 4 – Modeling and verification I (Chair: Sofiene Tahar) |
10:30–11:00 | Remark on Some Pi Variants | :
11:00–11:30 | Reasoning about Periodicity on Infinite Words | :
11:30–12:00 | On Equivalence Checking of Nondeterministic Finite Automata | :
12:15–13:45 | Lunch |
14:00–15:00 |
Keynote 3 (Chair: Sanjoy Baruah) Sanjit Seshia, University of California, Berkeley Towards Verified Artificial Intelligence |
15:00–16:00 | Session 5 – Formalization (Chair: Zhiping Shi) |
15:00–15:30 | Formal Analysis of Information Flow in HOL | :
15:30–16:00 | Formalizing SPARCv8 Instruction Set Architecture in Coq | :
16:00–16:30 | Tea break |
16:30–17:30 | Session 6 – Tools (Chair: Fu Song) |
16:30–17:00 | How to Efficiently Build a Front-End Tool for UPPAAL: A Model-Driven Approach | :
17:00–17:30 | PranCS: A Protocol and Discrete Controller Synthesis Tool | :
18:30–20:30 | Banquet |
Day 3:25 October 2017 | |
08:00–09:00 | Registration |
09:00–10:00 |
Keynote 4 (Chair: Xinyu Feng) Jean-Pierre Talpin, INRIA Compositional methods for cyber-physical system design |
10:00–10:30 | Tea break |
10:30–12:00 | Session 7 – Modeling and verification II (Chair: Zhishan Guo) |
10:30–11:00 | A Decomposition Method for Attractor Detection in Large Synchronous Boolean Networks | :
11:00–11:30 | Construction of Abstract State Graphs for Understanding Event-B Models | :
11:30–12:00 | A framework for modeling and verifying IoT communication protocols | :
12:00–12:15 | Closing |
12:15–13:45 | Lunch |