Program

The following is an overview of the program. A detailed draft program is available HERE.

Oct 24, 2023: Tutorial 1 (full day) and Tutorial 2 (half day in the afternoon)

Oct 25, 2023: ATVA 2023 Day 1 and PRDC Day 1, a reception is planned in the evening

Oct 26, 2023: ATVA 2023 Day 2 and PRDC Day 2, conference banquet is planned in the evening

Oct 27, 2023: ATVA 2023 Day 3 and ISACE Workshop

The following list of accepted papers for ATVA 2023 (in no particular order) and a dozen of published papers from ATVA 2022 and 2021 will be featured in the program:

  • Kasper Engelen, Guillermo Perez and Shrisha Rao. Graph-Based Reductions for Parametric and Weighted MDPs
  • Yushen Huang, Ertai Luo, Stanley Bak and Yifan Sun. On the Difficulty of Intersection Checking with Polynomial Zonotopes
  • Amit Gurung, Masaki Waga and Kohei Suenaga. Learning nonlinear hybrid automata from input–output time-series data
  • Omer Rappoport, Orna Grumberg and Yakir Vizel. Structure-Guided Solution of Constrained Horn Clauses
  • Suguman Bansal, Yong Li, Lucas Martinelli Tabajara, Moshe Vardi and Andrew Wells. On Strategies in Synthesis Over Finite Traces
  • Matin Ansaripour, Krishnendu Chatterjee, Thomas A. Henzinger, Mathias Lechner and Đorđe Žikelić. Learning Provably Stabilizing Neural Controllers for Discrete-Time Stochastic Systems
  • Oyendrila Dobe, Stefan Schupp, Ezio Bartocci, Borzoo Bonakdarpour, Axel Legay, Miroslav Pajic and Yu Wang. Lightweight Verification of Hyperproperties
  • Ye Tao, Wanwei Liu, Fu Song, Zhen Liang, Ji Wang and Hongxu Zhu. An Automata-Theoretic Approach to Synthesizing Binarized Neural Networks
  • Ying Liu, Andrea Turrini, Ernst Moritz Hahn, Bai Xue and Lijun Zhang. Scenario Approach for Parametric Markov Models
  • Steffan Sølvsten and Jaco van de Pol. Predicting Memory Demands of BDD Operations using Maximum Graph Cuts
  • Ethan Lew, Abdelrahman Hekal, Kostiantyn Potomkin, Niklas Kochdumper, Brandon Hencey, Stanley Bak and Sergiy Bogomolov. AutoKoopman: A Toolbox for Automated System Identification via Koopman Operator Linearization
  • Stefanie Mohr, Calvin Chau and Jan Kretinsky. Syntactic vs Semantic Linear Abstraction and Refinement of Neural Networks
  • Akshatha Shenoy, Sumanth Prabhu, Kumar Madhukar, Ron Shemer and Mandayam Srivas. Automated Property Directed Self Composition
  • Bernd Finkbeiner, Florian Kohn and Malte Schledjewski. Leveraging Static Analysis: An IDE for RTLola
  • Clément Aubert, Thomas Rubiano, Neea Rusch and Thomas Seiller. pymwp: A Static Analyzer Determining Polynomial Growth Bounds
  • Yong Li, Sven Schewe and Qiyi Tang. A novel family of finite automata for recognizing and learning $\omega$-regular languages
  • Oscar Ibarra and Ian McQuillan. On the Containment Problem for Deterministic Multicounter Machine Models
  • Kenny Ballou and Elena Sherman. Minimally Comparing Relational Abstract Domains
  • Bernd Finkbeiner, Jana Hofmann, Florian Kohn and Noemi Passing. Reactive Synthesis of Smart Contract Control Flows
  • Derek Egolf and Stavros Tripakis. Synthesis of Distributed Protocols by Enumeration Modulo Isomorphisms
  • David Lidell, Shaun Azzopardi, Nir Piterman and Gerardo Schneider. ppLTLTT: Temporal testing for pure-past linear temporal logic formulae
  • Haoqing Zhu, Yangge Li, Keyi Shen and Sayan Mitra. Parallel and Incremental Verification of Hybrid Automata with Ray and Verse
  • Zitong Zhou, Zixin Huang and Sasa Misailovic. AquaSense: Automated Sensitivity Analysis of Probabilistic Programs via Quantized Inference
  • Adam Chen, Tegan Brennan, Parisa Fathololumi, Eric Koskinen, Mihai Nicola and Jared Pincus. Better Predicate Pruning and Heuristics for Commutativity Synthesis
  • Kristina Miller, Christopher K. Zeitler, William Shen, Sayan Mitra and Mahesh Viswanathan. RTAEval : A framework for evaluating runtime assurance logic
  • Mohammad Afzal, Ashutosh Gupta and S Akshay. Using counterexamples to improve Robustness Verication in Neural Networks
  • Raven Beutner, Bernd Finkbeiner, Hadar Frenkel and Julian Siber. CATS: Checking Temporal Causes in Reactive Systems
  • J S Sajiv Kumar and Raghavan Komondoor. Controller synthesis for reactive systems with communication delay by formula translation
  • Arnd Hartmanns, Bram Kohlen and Peter Lammich. Fast Verified SCCs for Probabilistic Model Checking
  • Simon Lutz, Daniel Neider and Rajarshi Roy. Specification Sketching for Linear Temporal Logic
  • Shengjie Xu, Bineet Ghosh, Clara Hobbs, Enrico Fraccaroli, Parasara Sridhar Duggirala and Samarjit Chakraborty. Statistical Approach to Efficient and Deterministic Schedule Synthesis for Cyber-Physical Systems
  • Damien Busatto-Gaston, Debraj Chakraborty, Anirban Majumdar, Sayan Mukherjee, Guillermo Perez and Jean-Francois Raskin. Bi-Objective Lexicographic Optimization in Markov Decision Processes with Related Objectives
  • Parosh Aziz Abdulla, Mohamed Faouzi Atig, Frederik Meyer Bønneland, Sarbojit Das, Magnus Lång, Bengt Jonsson and Konstantinos Sagonas. Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
  • Dimitrios Thanos, Tim Coopmans and Alfons Laarman. Fast equivalence checking of quantum circuits of Clifford gates
  • Rafael Dewes and Rayna Dimitrova. Compositional High-Quality Synthesis
  • Morgan McColl, Callum McColl and Rene Hexel. Automatic Verification of High-Level Executable Models running on FPGAs
  • Nevatia Dhruv and Benjamin Monmege. An Automata Theoretic Characterization of Weighted First-Order Logic