Programme
Programme of main conferences from Monday to Thursday. Distinguished papers are highlighted in yellow and by asterisk.
Thursday 16 April
09:00
Guy Van Den Broeck: Symbolic Reasoning in the Age of Large Language Models
Chair: Sebastian Junges
Room: Sala 500
10:00
Coffee Break
Room: Expo Area
TACAS: CPS & Quantum
Chair: Kim Larsen
Room: Sala 500
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
Chair: Guillaume Ambal
Room: Sala Berlino
10:30
Satoshi Kura, Marco Gaboardi, Taro Sekiyama and Hiroshi Unno.
10:50
Han Xu and Di Wang.
11:30
Malo Revel, Thomas Genet and Thomas Jensen.
11:50
Nils Lommen and Jürgen Giesl.
12:10
Yasmin Sarita, Avaljot Singh, Shaurya Gomber, Gagandeep Singh and Mahesh Viswanathan.
SPIN
Chair:
Room: Sala Parigi
10:30
Invited Speaker: Christoph Matheja
11:30
Deductive Verification of Weak Memory Programs with View-based Protocols
Ömer Şakar, Soham Chakraborty, Marieke Huisman and Anton Wijs.
12:00
Crash-free Deductive Verifiers
Wander Nauta, Marcus Gerhold and Marieke Huisman (12:00).
12:30
Lunch Break
Room: Expo Area
TACAS: Model Checking & Hardware Verification
Chair: Rayna Dimitrova
Room: Sala 500
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.
16:00
AKR: A Model Checker for an Adaptative Probabilistic Knowing-How Logic
Valentin Cassano, Pablo Castro, Raul Fervari and Pedro R. D'Argenio.
Diversity, Equity, and Inclusion
Chair: Maurice ter Beek and Ferruccio Damiani
Room: Sala Londra
14:00
Test-Comp
Chair: Dirk Beyer
Room: Sala Madrid
14:00
SPIN
Chair:
Room: Sala Parigi
14:00
Invited Speaker: Laura Kovács
15:00
Recurrence-seeking Tests for Non-termination
Ravindra Metta, Hrishikesh Karmarkar, Kumar Madhukar, Supratik Chakraborty and Samarjit Chakraborty.
16:00
Coffee Break
Room: Expo Area
TACAS: SAT/SMT II
Chair: Natasha Sharygina
Room: Sala 500
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 Meeting
Chair: Dirk Beyer and Jan Strejček
Room: Sala Madrid
16:30