Program

09:00	Vijay Ganesh and Arie Gurfinkel Opening Remarks (abstract) PRESENTER: Vijay Ganesh
09:15	Nokiro Arai How to Solve Math Problems without Talent (abstract)

10:30-11:00Coffee Break

11:00-12:10 Session 2: Probabilistic and Quantum Systems 1

Chair:

Ichiro Hasuo

Location: MB 1.210

11:00	Alyzia-Maria Konsta, Alberto Lluch Lafuente and Christoph Matheja What should be observed for optimal reward in POMDPs? (abstract)
11:20	Alessandro Abate, Mirco Giacobbe and Diptarko Roy Stochastic Omega-Regular Verification and Control with Supermartingales (abstract)
11:40	Toru Takisaka, Libo Zhang, Changjiang Wang and Jiamou Liu Lexicographic Ranking Supermartingales with Lazy Lower Bounds (abstract)
12:00	Tobias Meggendorfer and Maximilian Weininger (Distinguished Paper) (Recorded) Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games (abstract)

12:10-14:00Lunch (Not Provided)

14:00-15:30 Session 3: Decision Procedures 1

Chair:

Ruzica Piskac

Location: MB 1.210

14:00	Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Işıl Dillig Split Gröbner Bases for Satisfiability Modulo Finite Fields (abstract)
14:20	Charlie Murphy and Zachary Kincaid Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement (abstract)
14:40	Peter Habermehl, Vojtěch Havlena, Michal Hečko, Lukáš Holík and Ondrej Lengal Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic (abstract)
15:00	Mengyu Zhao, Shaowei Cai and Yuhang Qian (Distinguished Paper) (Recorded) Distributed SMT Solving Based on Dynamic Variable-level Partitioning (abstract)
15:20	Nikolaj Bjørner and Lev Nachmanson Arithmetic Solving in Z3 (abstract)

15:30-16:00Coffee Break

16:00-18:10 Session 4: Concurrent, Distributed, and Quantum Systems

Chair:

Yu-Fang Chen

Location: MB 1.210

16:00	Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson and Konstantinos Sagonas Parsimonious Optimal Dynamic Partial Order Reduction (abstract)
16:20	Ziqing Luo and Stephen F. Siegel Collective Contracts for Message-Passing Parallel Programs (abstract)
16:40	Eden Frenkel, Tej Chajed, Oded Padon and Sharon Shoham Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas (abstract)
17:00	Noah Bertram, Tean Lai and Justin Hsu Verifying Cake Cutting, Faster (abstract)
17:20	Jingyi Mei, Marcello Bonsangue and Alfons Laarman Simulating Quantum Circuits by Model Counting (abstract)
17:40	Lukas Armborst, Pieter Bos, Lars van den Haak, Marieke Huisman, Robert Rubbens, Ömer Sakar and Philip Tasche The VerCors Verifier: a Progress Report (abstract)
17:50	James R. Wilcox, Yotam M. Y. Feldman, Oded Padon and Sharon Shoham mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic (abstract)

18:10-19:30 Reception

Chair:

Arie Gurfinkel

Location: MB9 ABCD

Thursday, July 25th

View this program: with abstracts session overview talk overview

08:30-09:00Breakfast

09:00-10:10 Session 5: Decision Procedures 2

Chair:

Alessandro Cimatti

Location: MB 1.210

09:00	Aina Niemetz, Mathias Preiner and Yoni Zohar Scalable Bit-Blasting with Abstractions (abstract)
09:20	Joseph Reeves, Marijn Heule and Randal Bryant From Clauses to Klauses (abstract)
09:40	Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen and Kuldeep S. Meel (Distinguished Paper) Formally Certified Approximate Model Counting (abstract)
10:00	Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt CaDiCaL 2.0 (abstract)

10:10-10:30 Session 6: Machine Learning and Neural Networks 1

Chair:

Ravi Mangal

Location: MB 1.210

10:10	Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretinsky, Stefanie Mohr and Sabine Rieder Monitizer: Automating Design and Evaluation of Neural Network Monitors (abstract)
10:20	Haoze Wu, Omri Isac, Aleksandar Zeljić, Teruhiro Tagomori, Matthew Daggitt, Wen Kokke, Idan Refaeli, Guy Amir, Kyle Julian, Shahaf Bassan, Pei Huang, Ori Lahav, Min Wu, Min Zhang, Ekaterina Komendantskaya, Guy Katz and Clark Barrett Marabou 2.0: A Versatile Formal Analyzer of Neural Networks (abstract)

10:30-11:00Coffee Break

11:00-12:00 Session 7: CAV Keynote: Lean 4: Bridging Formal Mathematics and Software Verification

Chair:

Vijay Ganesh

Location: MB 1.210

11:00

Leonardo de Moura

Lean 4: Bridging Formal Mathematics and Software Verification (abstract)

12:00-14:00Lunch (Not Provided)

14:00-15:30 Session 8: Software Verification 1

Chair:

Grigory Fedyukovich

Location: MB 1.210

14:00	Arjun Pitchanathan, Albert Cohen, Oleksandr Zinenko and Tobias Grosser Strided Difference Bound Matrices (abstract)
14:20	Chenglin Wang and Fangzhen Lin On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches (abstract)
14:40	Marco Eilers, Malte Schwerhoff and Peter Müller Verification Algorithms for Automated Separation Logic Verifiers (abstract)
15:00	Michele Chiari, Luca Geatti, Nicola Gigante and Matteo Pradella SMT-based Symbolic Model-Checking for Operator Precedence Languages (abstract)
15:20	Chanhee Cho, Yi Zhou, Jay Bosamiya and Bryan Parno (Distinguished Paper) A Framework for Debugging Automated Program Verification Proofs via Proof Actions (abstract)

15:30-16:00Coffee Break

16:00-18:20 Session 9: Synthesis and Repair

Chair:

Jana Hofmann

Location: MB 1.210

16:00	Anders Miltner, Ziteng Wang, Swarat Chaudhuri and Isil Dillig Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton (abstract)
16:20	Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger and Julian Siber Synthesis of Temporal Causality (abstract)
16:40	Philippe Heim, Satya Prakash Nayak, Rayna Dimitrova and Anne-Kathrin Schmuck Localized Attractor Computations for Infinite-State Games (abstract)
17:00	Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour and Bernd Finkbeiner Syntax-Guided Automated Program Repair For Hyperproperties (abstract)
17:20	Yi Lin, Moshe Vardi and Lucas Martinelli Tabajara Dynamic Programming for Symbolic Boolean Realizability and Synthesis (abstract)
17:40	Bernd Finkbeiner, Niklas Metzger and Yoram Moses Information Flow guided Synthesis with Unbounded Communication (abstract)
18:00	Keith J.C. Johnson, Andrew Reynolds, Thomas Reps and Loris D'Antoni The SemGuS Toolkit (abstract)
18:10	Swen Jacobs The Reactive Synthesis Competition (SYNTCOMP) Report

18:20-18:30Break

18:30-19:30 Session 10: Logic Lounge

Chair:

Ruzica Piskac

Location: MB 1.210

18:30

Scott Shapiro

Realizing Leibniz’s Dream (abstract)

Friday, July 26th

View this program: with abstracts session overview talk overview

08:30-09:00Breakfast

09:00-10:30 Session 11: Learning

Chair:

Hongce Zhang

Location: MB 1.210

09:00	Alessandro Abate, Mirco Giacobbe and Yannik Schnitzer Bisimulation Learning (abstract)
09:20	Mojtaba Valizadeh, Nathanael Fijalkow and Martin Berger LTL learning on GPUs (abstract)
09:40	Taylor Dohmen, Mateo Perez, Fabio Somenzi and Ashutosh Trivedi (Distinguished Paper) Regular Reinforcement Learning (abstract)
10:00	Yuning Wang and He Zhu Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models (abstract)
10:20	Jan Baumeister, Bernd Finkbeiner, Florian Kohn, Sebastian Schirmer, Christoph Torens, Florian Löhr and Guido Manfredi Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned (abstract)

10:30-11:00Coffee Break

11:00-12:00 Session 12: CAV Award

Chair:

Alessandro Cimatti

Location: MB 1.210

11:00

Cav Award

CAV Award Talk

12:00-14:00Lunch (Not Provided)

14:00-15:30 Session 13: Software Verification 2

Chair:

Jingbo Wang

Location: MB 1.210

14:00	Yannick Stade, Sarah Tilscher and Helmut Seidl The Top-Down Solver Verified: Building Confidence in Static Analyzers (abstract)
14:20	Dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall and Mikael Brockman (Recorded) hevm, a Fast Symbolic Execution Framework for EVM Bytecode (abstract)
14:30	Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt and Natasha Sharygina SolTG: A CHC-based Solidity Test Case Generator (abstract)
14:40	Shaowei Zhu and Zachary Kincaid (Recorded) Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates (abstract)
15:00	Shenghao Yuan, Frédéric Besson and Jean-Pierre Talpin (Recorded) End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT (abstract)
15:20	Sujit Muduli, Rohan Padulkar and Subhajit Roy (Distinguished Paper) (Recorded) Interactive Theorem Proving modulo Fuzzing (abstract)

15:30-16:00Coffee Break

16:00-17:00 Session 14: Hardware Model Checking

Chair:

Natasha Sharygina

Location: MB 1.210

16:00	Kenneth McMillan Toward Liveness Proofs at Scale (abstract)
16:20	Yechuan Xia, Alessandro Cimatti, Alberto Griggio and Jianwen Li Avoiding the Shoals - A New Approach to Liveness Checking (abstract)
16:40	Franz Brauße, Zurab Khasidashvili and Konstantin Korovin SMLP: Symbolic Machine Learning Prover (abstract)
16:50	Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi and Kristin Yvonne Rozier Symbolic Model-Checking Intermediate-Language Tool Suite (abstract)

17:00-18:10 Session 15: Runtime Verification and Monitoring

Chair:

Borzoo Bonakdarpour

Location: MB 1.210

17:00	Zhendong Ang and Umang Mathur Predictive Monitoring with Strong Trace Prefixes (abstract)
17:20	Raik Hipler, Hannes Kallwies, Martin Leucker and César Sánchez General Anticipatory Runtime Verification (abstract) PRESENTER: Hannes Kallwies
17:40	François Hublet, Leonardo Lima, David Basin, Srdjan Krstic and Dmitriy Traytel Proactive Real-Time First-Order Enforcement (abstract)
18:00	Anna Becchi, Alessandro Cimatti and Giuseppe Scaglione Testing the migration from analog to software-based Railway Interlocking Systems (abstract)

18:10-19:00 Session 16: CAV Business Meeting

Chair:

Arie Gurfinkel

Location: MB 1.210

19:30-21:00 CAV Banquet

CAV Banquet at Vieux Port Steakhouse located at 405 rue Saint-Jean-Baptiste, Montréal, QC, H2Y 2Z7

map

Note that this is a different entrance than the main entrace for the restaurant.

Chair:

Arie Gurfinkel

Location: Vieux Port Steakhouse

Saturday, July 27th

View this program: with abstracts session overview talk overview

08:30-09:00Breakfast

09:00-10:30 Session 17: Cyberphysical, Hybrid, and Complex Systems

Chair:

Bernd Finkbeiner

Location: MB 1.210

09:00	Florian Lercher and Matthias Althoff Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems (abstract)
09:20	Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo Optimization-Based Model Checking for Complex STL Specifications (abstract)
09:40	Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott Shapiro and Ruzica Piskac soid: A Tool for Legal Accountability for Automated Decision Making (abstract)
09:50	Dejin Ren, Zhen Liang, Chenyu Wu, Jianqiang Ding, Taoran Wu and Bai Xue (Recorded) Inner-approximate Reachability Computation via Zonotopic Boundary Analysis (abstract)
10:10	Jiawan Wang, Wenxia Liu, Muzimiao Zhang, Jiaqi Wei, Yuhui Shi, Lei Bu and Xuandong Li (Recorded) Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs (abstract)

10:30-11:00Coffee Break

11:00-12:00 Session 18: CAV Keynote: The Art of SMT Solving

Chair:

Vijay Ganesh

Location: MB 1.210

11:00

Erika Abraham

The Art of SMT Solving (abstract)

12:00-14:00Lunch (Not Provided)

14:00-15:30 Session 19: Probabilistic and Quantum Systems 2

Chair:

Xujie Si

Location: MB 1.210

14:00	Shaowei Zhu and Yunbo Zhang (Recorded) Probabilistic Access Policies with Automated Reasoning Support (abstract)
14:20	Kazuki Watanabe, Marck van der Vegt, Sebastian Junges and Ichiro Hasuo Compositional Value Iteration with Pareto Caching (abstract)
14:40	Peng Yan, Hanru Jiang and Nengkun Yu Approximate Relational Reasoning for Quantum Programs (abstract)
15:00	Aochu Dai and Mingsheng Ying QReach: A Reachability Analysis Tool for Quantum Markov Chains (abstract)
15:10	Ji Guan, Yuan Feng, Andrea Turrini and Mingsheng Ying (Recorded) Measurement-based Verification of Quantum Markov Chains (abstract)

15:30-16:00Coffee Break

16:00-18:00 Session 20: Machine Learning and Neural Networks 2

Chair:

Erika Abraham

Location: MB 1.210

16:00	Yixuan Li, Julian Parsert and Elizabeth Polgreen Guiding Enumerative Program Synthesis with Large Language Models (abstract)
16:20	Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong and Min Zhang Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems (abstract)
16:40	Ruihan Zhang and Jun Sun Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors (abstract)
17:00	Yuval Shapira, Naor Wiesel, Shahar Shabelman and Dana Drachsler-Cohen Boosting Few-Pixel Robustness Verification via Covering Verification Designs (abstract)
17:20	Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic and Georg Weissenbacher (Recorded) Verifying Global Two-Safety Properties in Neural Networks with Confidence (abstract)
17:40	Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung and Cong Tian (Recorded) Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification (abstract)