Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Thursday 16 April
10:00
Coffee Break
TACAS: CPS & Quantum
Room:
10:30
Driving by Disproof: A Practical Model Checking Approach to Fleet Coordination
Lukas König, Christian Schildwächter, Michaela Klauck and Christian Heinzemann.
10:50
VeriLHyS: a Framework for LTL Specification and Verification of Hybrid Systems
Ludovico Battista, Stefano Tonetta and Gianni Zampedri.
11:10
TEMPORA: Efficient Verification of Metric Temporal Properties with Past in Pointwise Semantics
S. Akshay, Prerak Contractor, Paul Gastin, R Govind and B Srivathsan.
11:30
Trace Repair Using Temporal Behavior Trees
Sebastian Schirmer, Philipp Schitz, Johann C. Dauer, Bernd Finkbeiner and Sriram Sankaranarayanan.
11:50
Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting
Wei-Jia Huang, Jingyi Mei, Alfons Laarman, Yu-Fang Chen, Christophe Chareton, Kai-Min Chung and Min-Hsiu Hsieh.
12:10
Error-Tolerant Quantum State Discrimination: Optimization and Quantum Circuit Synthesis
Chien-Kai Ma, Bo-Hung Chen, Tian-Fu Chen, Dah-Wei Chiou and Jie-Hong Roland Jiang.
ESOP: Analysis
Room:
10:30
A Category-Theoretic Framework for Dependent Effect Systems
Satoshi Kura, Marco Gaboardi, Taro Sekiyama and Hiroshi Unno.
10:50
Dependently-Typed AARA: A Non-Affine Approach for Resource Analysis of Higher-Order Programs
Han Xu and Di Wang.
11:10
Max-Policy Iteration, Revisited
David Monniaux and Helmut Seidl.
11:30
Complete Abstractions for Verification of Polymorphic Functions with Equality
Malo Revel, Thomas Genet and Thomas Jensen.
11:50
Modular Automatic Complexity Analysis of Recursive Integer Programs
Nils Lommen and Jürgen Giesl.
12:10
Efficient Ranking Function-Based Termination Analysis via Bidirectional Decompositional Search
Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh and Mahesh Viswanathan.
SPIN
Chair:
Room:
10:30
12:30
Lunch Break
TACAS: Model Checking & Hardware Verification
Room:
14:00
CTL* Model Checking on Infinite Families of Finite-State Labeled Transition Systems
Roberto Pettinau and Christoph Matheja.
14:20
Verifying First-Order Temporal Properties of Infinite States Systems via Timers and Rankings
Raz Lotan, Neta Elad, Oded Padon and Sharon Shoham.
14:40
Revisiting Stateful Partial-Order Reduction
Frédéric Herbreteau, Gérald Point and Igor Walukiewicz.
15:00
Deconstructing Subset Construction: Reducing While Determinizing
Markus Frohme and John Nicol.
15:20
ReVEAL: GNN-Guided Reverse Engineering for Formal Verification of Optimized Multipliers
Chen Chen, Daniela Kaufmann, Chenhui Deng, Zhan Song, Hongce Zhang and Cunxi Yu
15:40
EvolveGen: Algorithmic Level Hardware Model Checking Benchmark Generation through Reinforcement Learning
Guangyu Hu, Xiaofeng Zhou, Wei Zhang and Hongce Zhang.
Diversity, Equity, and Inclusion
Chair:
Room:
14:00
TEST-COMP
Chair:
Room:
14:00
SPIN
Chair:
Room:
14:00
16:00
Coffee Break
TACAS: SAT/SMT II
Room:
16:30
Parallel SMT Solving via Iterative Tree Partitioning
Tomáš Kolárik, Antti E.J. Hyvärinen, Seyedmasoud Asadzadeh and Natasha Sharygina.
16:50
Massively Parallel Bit-Precise Verification with Bitwuzla and Mallob
Dominik Schreiber, Aina Niemetz and Mathias Preiner.
17:10
Exploring the SMT-LIB Benchmark Library
Hans-Jörg Schurr, François Bobot, Mathias Preiner, Aina Niemetz, Pascal Fontaine, Cesare Tinelli and Clark Barrett.
17:30
SMT(LIA) Sampling with High Diversity
Yong Lai, Junjie Li and Chuan Luo.
17:50
BDD-Based Formula Approximations for Quantified Bit-Vector Satisfiability
Jakub Horák and Martin Jonáš.
18:10
SMTScope: Automated and Efficient Analysis of SMT Traces
Jonáš Fiala and Peter Müller.
SV-Comp and Test-Comp Community Building
Chair:
Room:
16:30
SPIN
Chair:
Room:
16:30