Venue: All except the first keynote talk (on Oct 25 morning) will take place at Level 5, School of Computing and Information Systems 2 (also known as School of Economics), Singapore Management University. Kindly refer to the map below for the exact location (GPS coordinate: 1.2979140942901206, 103.84898382636581).
The first keynote talk (on Oct 25 morning) will take place at Level 2, Seminar Room 2-16, SMU Yong Pung How School of Law, Singapore Management University. Kindly refer to the map below for the exact location (GPS coordinate: 1.294990465618122, 103.84946280514102).
Proceedings are available at Springer LNCS:
Oct 24, 2023: Tutorials (Free with Any Registration)
Event: Tutorial 1
Time: 9:00 to 12:00 and 14:00 to 17:00
Venue: CTE Scape, School of Computing and Information Systems 2, Singapore Management University
Description: “The K Framework: A tool kit for language semantics and verification” by Runtime Verification Inc.
12:00 to 14:00: Lunch will be provided for those registered attendees at level 5 of School of Computing and Information Systems 2, Singapore Management University
Event: Tutorial 2
Time: 14:00 to 17:00
Venue: Seminar Room 5-2, Level 5, School of Computing and Information Systems 2, Singapore Management University
Description: “Developing Assurance Cases with AdvoCATE”, by Ewen Denney (NASA Ames Research Center, USA)
ATVA 2023 Day One, Oct 25, 2023
Venue: The opening address and keynote 1 will take place at Seminar Room 2-16, SMU Yong Pung How School of Law, Singapore Management University. The remaining sessions will take place at Seminar Room 5-1, School of Computing and Information Systems 2, Singapore Management University. Tea/coffee, and lunch will be provided outside of the seminar room at level 5, School of Computing and Information Systems 2. The reception will be provided at School of Computing and Information Systems 1 Alcove (at baseline).
8:45 – 9:00: Opening Address (by Étienne André, Jun Sun, Zhe Hou, and Yun Lin)
9:00 – 10:00: Keynote 1 (chaired by Jinsong Dong)
“Correct and Efficient Policy Monitoring, a Retrospective” (by David Basin, ETH)
10:00 – 10:30: Tea/Coffee Break
10:30 to 12:10: Automata (chaired by Xiaofei Xie)
10:30 to 10:50: Learning nonlinear hybrid automata from input-output time-series data (Amit Gurung, Masaki Waga and Kohei Suenaga)
10:50 to 11:10: A novel family of finite automata for recognizing and learning omega-regular languages (Yong Li, Sven Schewe and Qiyi Tang)
11:10 to 11:30: On the Containment Problem for Deterministic Multicounter Machine Models (Oscar Ibarra and Ian McQuillan)
11:30 to 11:50: Parallel and Incremental Verification of Hybrid Automata with Ray and Verse (Haoqing Zhu, Yangge Li, Keyi Shen and Sayan Mitra)
11:50 to 12:10: An Automata Theoretic Characterization of Weighted First-Order Logic (Nevatia Dhruv and Benjamin Monmege)
12:10 to 13:45: Lunch
13:45 to 15:05: Probabilistic Systems (chaired by Djordje Zikelic)
13:45 to 14:05: Graph-Based Reductions for Parametric and Weighted MDPs (Kasper Engelen, Guillermo Perez and Shrisha Rao)
14:05 to 14:25: Scenario Approach for Parametric Markov Models (Ying Liu, Andrea Turrini, Ernst Moritz Hahn, Bai Xue and Lijun Zhang)
14:25 to 14:45: Fast Verified SCCs for Probabilistic Model Checking (Arnd Hartmanns, Bram Kohlen and Peter Lammich)
14:45 to 15:05: Bi-Objective Lexicographic Optimization in Markov Decision Processes with Related Objectives (Damien Busatto-Gaston, Debraj Chakraborty, Anirban Majumdar, Sayan Mukherjee, Guillermo Perez and Jean-Francois Raskin)
15:05 to 15:35 Session 3: Tools Papers 1 (chaired by Yushen Huang)
15:05 to 15:15: AutoKoopman: A Toolbox for Automated System Identification via Koopman Operator Linearization (Ethan Lew, Abdelrahman Hekal, Kostiantyn Potomkin, Niklas Kochdumper, Brandon Hencey, Stanley Bak and Sergiy Bogomolov)
15:15 to 15:25: Leveraging Static Analysis: An IDE for RTLola (Bernd Finkbeiner, Florian Kohn and Malte Schledjewski)
15:25 to 15:35: pymwp: A Static Analyzer Determining Polynomial Growth Bounds (Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller)
15:35 to 16:00: Tea/Coffee Break
16:00 to 18:00: Greeting from the past (chaired by Ian McQuillan)
16:00 to 16:20: Dynamic Shielding for Reinforcement Learning in Black-Box Environments (Masaki Waga, Ezequiel Castellano, Sasinee Pruekprasert, Stefan Klikovits, Toru Takisaka, Ichiro Hasuo)
16:20 to 16:40: Optimistic and Topological Value Iteration for Simple Stochastic Games (Muqsit Azeem, Alexandros Evangelidis, Jan Křetínský, Alexander Slivinskiy, Maximilian Weininger)
16:40 to 17:00: Fence Synthesis under the C11 Memory Model (Sanjana Singh, Divyanjali Sharma, Ishita Jaju, Subodh Sharma)
17:00 to 17:20: Symbolic Runtime Verification for Monitoring Under Uncertainties and Assumptions (Hannes Kallwies, Martin Leucker, Cesar Sanchez)
17:20 to 17:40: Event-B Refinement for Continuous Behaviours Approximation (Guillaume Dupont, Yamine Aït-Ameur, Marc Pantel & Neeraj K. Singh)
17:40 to 18:00: Verification of SMT Systems with Quantifiers (Alessandro Cimatti, Alberto Griggio & Gianluca Redondi)
18:00 – 20:00: Conference Reception
ATVA 2023 Day Two, Oct 26, 2023
Venue: All sessions will take place at Seminar Room 5-2, School of Computing and Information Systems 2, Singapore Management University. Tea/coffee, and lunch will be provided outside of the seminar room at level 5, School of Computing and Information Systems 2. The buses for the conference dinner will leave from level 1 of School of Computing and Information Systems 2 (pick up near the security) at 6pm; and will leave for the conference venue from Night Safari at 10:00pm.
09:00 -10:00: Keynote 2 (chaired by Étienne André)
“Dynamic Assurance Cases for Machine-learning based Autonomous Systems” by Ewen Denney, NASA Ames Research Center
10:00 – 10:30: Tea/Coffee Break
10:30 to 12:30: Synthesis (chaired by Borzoo Bonakdarpour)
10:30 to 10:50: Model Checking Strategies from Synthesis Over Finite Traces (Suguman Bansal, Yong Li, Lucas Martinelli Tabajara, Moshe Vardi and Andrew Wells)
10:50 to 11:10: Reactive Synthesis of Smart Contract Control Flows (Bernd Finkbeiner, Jana Hofmann, Florian Kohn and Noemi Passing)
11:10 to 11:30: Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms (Derek Egolf and Stavros Tripakis)
11:30 to 11:50: Controller synthesis for reactive systems with communication delay by formula translation (J S Sajiv Kumar and Raghavan Komondoor)
11:50 to 12:10: Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical Systems (Shengjie Xu, Bineet Ghosh, Clara Hobbs, Enrico Fraccaroli, Parasara Sridhar Duggirala and Samarjit Chakraborty)
12:10 to 12:30: Compositional High-Quality Synthesis (Rafael Dewes and Rayna Dimitrova)
12:30 to 13:45: Lunch
13:45 to 15:05: Neural networks (chaired by Andre Etienne)
13:45 to 14:05: Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems (Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner and Ðorđe Žikelić
14:05 to 14:25: An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks (Ye Tao, Wanwei Liu, Fu Song, Zhen Liang, Ji Wang and Hongxu Zhu)
14:25 to 14:45: Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks (Calvin Chau, Jan Kretinsky and Stefanie Mohr)
14:45 to 15:05: Using Counterexamples to Improve Robustness Verification in Neural Networks (Mohammad Afzal, Ashutosh Gupta and S Akshay)
15:05 to 15:45: Tool Papers 2 (chaired by Chris Poskitt)
15:05 to 15:15: ppLTLTT: Temporal testing for pure-past linear temporal logic formulae (David Lidell, Shaun Azzopardi, Nir Piterman and Gerardo Schneider)
15:15 to 15:25: AquaSense: Automated Sensitivity Analysis of Probabilistic Programs via Quantized Inference (Zitong Zhou, Zixin Huang and Sasa Misailovic)
15:25 to 15:35: RTAEval : A framework for evaluating runtime assurance logic (Kristina Miller, Christopher K. Zeitler, William Shen, Sayan Mitra and Mahesh Viswanathan)
15:35 to 15:45: Checking and Sketching Causes on Temporal Sequences (Raven Beutner, Bernd Finkbeiner, Hadar Frenkel and Julian Siber)
15:45 to 16.15: Tea/Coffee Break
16:15 to 17:15: Data Structures and Heuristics (chaired by Alfons Laarman)
16:15 to 16:35: On the Difficulty of Intersection Checking with Polynomial Zonotopes (Yushen Huang, Ertai Luo, Stanley Bak and Yifan Sun)
16:35 to 16:55: Predicting Memory Demands of BDD Operations using Maximum Graph Cuts (Steffan Solvsten and Jaco van de Pol)
16:55 to 17:15: Better Predicates and Heuristics for Improved Commutativity Synthesis (Adam Chen, Parisa Fathololumi, Mihai Nicola, Jared Pincus, Tegan Brennan and Eric Koskinen)
18:00 to 21:00: Conference Banquet
ATVA 2023 Day Three, Oct 27, 2023
Venue: All sessions will take place at Seminar Room 5-2, School of Computing and Information Systems 2, Singapore Management University. Tea/coffee, and lunch will be provided outside of the seminar room at level 5, School of Computing and Information Systems 2.
09:00 – 10:00: Keynote 3 (chaired by Sun Jun)
“Privacy in Machine Learning” by Reza Shokri, NUS
10:00 – 10:30: Tea/Coffee Break
10:30 to 12:30: Verification of Programs and Hardware (chaired by Raghavan Komondoor)
10:30 to 10:50: Structure-Guided Solution of Constrained Horn Clauses (Omer Rappoport, Orna Grumberg and Yakir Vizel)
10:50 to 11:10: Automated Property Directed Self Composition (Akshatha Shenoy, Sumanth Prabhu, Kumar Madhukar, Ron Shemer and Mandayam Srivas)
11:10 to 11:30: Minimally Comparing Relational Abstract Domains (Kenny Ballou and Elena Sherman)
11:30 to 11:50: Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs (Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bonneland, Sarbojit Das, Bengt Jonsson, Magnus Lång and Konstantinos Sagonas)
11:50 to 12:10: Fast equivalence checking of quantum circuits of Clifford gates (Dimitrios Thanos, Tim Coopmans and Alfons Laarman)
12:10 to 12:30: Automatic Verification of High-Level Executable Models Running on FPGAs (Morgan McColl, Callum McColl and Rene Hexel)
12:30 to 13:45: Lunch
13:45 to 15:25: Temporal logics and More (chaired by Ichiro Hasuo)
13:45 to 14:05: Lightweight Verification of Hyperproperties (Oyendrila Dobe, Stefan Schupp, Ezio Bartocci, Borzoo Bonakdarpour, Axel Legay, Miroslav Pajic and Yu Wang)
14:05 to 14:25: Specification Sketching for Linear Temporal Logic (Simon Lutz, Daniel Neider and Rajarshi Roy)
14:25 to 14:45: Proving SIFA Protection of Masked Redundant Circuits (Vedad Hadzic, Robert Primas, Roderick Bloem)
14:45 to 15:05: Temporal Causality in Reactive Systems (Norine Coenen, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Niklas Metzger, Julian Siber)
15:05 to 15:25: Checking Scheduling-induced Violations of Control Safety Properties (Anand Yeolekar, Ravindra Metta, Clara Hobbs & Samarjit Chakraborty)
15:25 to 15:30: Closing Session: Introducing ATVA 2024
15:30 to 16:00: Tea/Coffee Break