CAV PROGRAM
Days: Sunday, August 7th Monday, August 8th Tuesday, August 9th Wednesday, August 10th
Sunday, August 7th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 85A: Formal Methods for Probabilistic Programs
Chair:
Location: Taub 1
| 09:00 | Data-Driven Invariant Learning for Probabilistic Programs (abstract)   PRESENTER: Subhajit Roy |
| 09:20 | Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs (abstract) PRESENTER: Đorđe Žikelić |
| 09:40 | Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions (abstract) PRESENTER: Lutz Klinkenberg |
| 10:00 | Abstraction-Refinement for Hierarchical Probabilistic Models (abstract) PRESENTER: Sebastian Junges |
10:30-11:00Coffee Break
11:00-12:00 Session 89: Keynote
Chair:
Location: Churchill Auditorium
| 11:00 | Harnessing the Power of Formal Verification for the $Trillion Chip Design Industry (abstract) |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, ITP).
14:00-15:30 Session 90A: Formal Methods for Neural Networks
Chair:
Location: Taub 1
| 14:00 | Shared Certificates for Neural Network Verification (abstract)  PRESENTER: Dimitar I. Dimitrov |
| 14:20 | Example Guided Synthesis of Linear Approximations for Neural Network Verification (abstract) PRESENTER: Brandon Paulsen |
| 14:40 | Verifying Neural Networks Against Backdoor Attacks (abstract) PRESENTER: Long H. Pham |
| 15:00 | Trainify: A CEGAR-Driven Training and Verification Framework for Verifiable Deep Reinforcement Learning (abstract) PRESENTER: Jiaxu Tian |
| 15:20 | Neural Network Robustness as a Verification Property: A Principled Case Study (abstract) PRESENTER: Marco Casadio |
15:30-16:00Coffee Break
16:00-17:30 Session 92A: Software Verification and Model Checking
Chair:
Location: Taub 1
| 16:00 | The Lattice-Theoretic Essence of Property Directed Reachability Analysis (abstract) PRESENTER: Mayuko Kori |
| 16:20 | Affine Loop Invariant Generation via Matrix Algebra (abstract) PRESENTER: Yucheng Ji |
| 16:40 | Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes (abstract) PRESENTER: Wael-Amine Boutglay |
| 17:00 | Proof-guided Underapproximation Widening for Bounded Model Checking (abstract)  PRESENTER: Subhajit Roy |
| 17:20 | SolCMC: Solidity Compiler’s Model Checker (abstract) PRESENTER: Leonardo Alt |
17:30-18:45 Session 93: Logic Lounge: Future of Autonomous Driving; Keynote by Shai Shalev-Shwartz (Mobileye and The Hebrew University of Jerusalem); Panel: Gila Kamhi (Intel, Haifa), Sanjit Seshia (UC Berkeley)
Chair:
Location: Churchill Auditorium
Monday, August 8th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
09:00-10:30 Session 94A: Hyperproperties and Security
Chair:
Location: Taub 1
| 09:00 | Software Verification of Hyperproperties Beyond k-Safety (abstract) PRESENTER: Raven Beutner |
| 09:20 | A Scalable Shannon Entropy Estimator (abstract) PRESENTER: Kuldeep S. Meel |
| 09:40 | PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation (abstract) PRESENTER: Yuxin Fan |
| 10:00 | Explaining Hyperproperty Violations (abstract) PRESENTER: Julian Siber |
| 10:20 | Distilling Constraints in Zero-Knowledge Protocols (abstract) PRESENTER: Miguel Isabel |
10:30-11:00Coffee Break
11:00-12:30 Session 96A: Invited Talk: A Billion SMT Queries a Day (Neha Rungta)
Chair:
Location: Taub 1
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).
14:00-15:30 Session 97A: Formal Methods for Hardware, Cyber-Physical and Hybrid Systems
Chair:
Location: Taub 1
| 14:00 | Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption (abstract) PRESENTER: Ryotaro Banno |
| 14:20 | Abstraction Modulo Stability for Reverse Engineering (abstract) PRESENTER: Anna Becchi |
| 14:40 | Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement (abstract) PRESENTER: Ethan Lew |
| 15:00 | RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems (abstract) PRESENTER: Sylvie Putot |
| 15:10 | STLmc: Robust STL Model Checking of Hybrid Systems using SMT (abstract) PRESENTER: Kyungmin Bae |
| 15:20 | UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (abstract) PRESENTER: Elizabeth Polgreen |
15:30-16:00Coffee Break
16:00-17:30 Session 98A: Probabilistic Techniques
Chair:
Location: Taub 1
| 16:00 | PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP (abstract) PRESENTER: Chaitanya Agarwal |
| 16:20 | Sampling-Based Verification of CTMCs with Uncertain Rates (abstract) PRESENTER: Thom Badings |
| 16:40 | Playing Against Fair Adversaries in Stochastic Games with Total Rewards (abstract) PRESENTER: Pablo Castro |
| 17:00 | Automated Expected Amortised Cost Analysis of Probabilistic Data Structures (abstract) PRESENTER: Lorenz Leutgeb |
| 17:20 | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers (abstract) PRESENTER: Aina Niemetz |
18:30-20:30 Walking tour (at Haifa)
pickup at 18:00 from the Technion (Tour at Haifa, no food will be provided)
Tuesday, August 9th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
10:30-11:00Coffee Break
11:00-12:30 Session 102A: Automata and Logic
Chair:
Location: Taub 1
| 11:00 | FORQ-based Language Inclusion Formal Testing (abstract) PRESENTER: Kyveli Doveri |
| 11:20 | Sound Automation of Magic Wands (abstract) PRESENTER: Thibault Dardinier |
| 11:40 | Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition (abstract) PRESENTER: Yong Li |
| 12:00 | From Spot 2.0 to Spot 2.10: What's New? (abstract) PRESENTER: Alexandre Duret-Lutz |
| 12:10 | Complementing Büchi Automata with Ranker (abstract) PRESENTER: Barbora Šmahlíková |
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, NMR, IJCAR, ITP).
13:00-14:00 Session 103: Tool Demonstrations
Tool demonstrations for:
- STLmc: Robust STL Model Checking of Hybrid Systems using SMT (13:00-13:30)
- UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis (13:30-14:00)
Location: Taub entrance floor lobby
14:00-16:00 Session 104A: Deductive Verification and Decision Procedures
Chair:
Location: Taub 1
| 14:00 | Even Faster Conflicts and Lazier Reductions for String Solvers (abstract) PRESENTER: Andres Noetzli |
| 14:20 | Local Search For SMT on Linear Integer Arithmetic (abstract) PRESENTER: Shaowei Cai |
| 14:40 | Reasoning about Data Trees using CHCs (abstract) PRESENTER: Gennaro Parlato |
| 15:00 | Verified Erasure Correction in Coq with MathComp and VST (abstract) PRESENTER: Joshua M. Cohen |
| 15:20 | End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers (abstract) PRESENTER: Shenghao Yuan |
| 15:40 | Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols (abstract) PRESENTER: Joonwon Choi |
16:00-16:30Coffee Break
16:30-17:30 Session 108: Plenary
Chair:
Location: Churchill Auditorium
| 16:30 | SMT-based Verification of Distributed Network Control Planes (abstract) |
17:30-18:30 Session 109: Business Meeting
17:30-17:45 - As part of the buisneess meeting we will have a 15 minutes presentation by Pavithra Prabhakar.
Title: Formal Methods and Verification Programs and International Partnerships at NSF.
The talk will provide a brief overview of the funding opportunities at the US National Science Foundation related to the area of formal methods and computer aided verification. International partnerships and opportunities for participation of the broader scientific community will be highlighted.
Chairs:
Location: Taub 1
Wednesday, August 10th
View this program: with abstractssession overviewtalk overviewside by side with other conferences
08:30-09:00Coffee & Refreshments
10:30-11:00Coffee Break
11:00-12:30 Session 112A: Invited Talk: Program Verification with Constrained Horn Clauses (Arie Gurfinkel)
Chair:
Location: Taub 1
12:30-14:00Lunch Break
Lunches will be held in Taub lobby (CAV, CSF) and in The Grand Water Research Institute (DL, IJCAR, ITP).
13:00-14:00 Session 114: Tool Demonstrations
Tool demonstrations for:
- From Spot 2.0 to Spot 2.10: What's New? (13:00-13:30)
- Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (13:30-14:00)
Location: Taub entrance floor lobby
14:00-15:30 Session 115A: Machine Learning
Chair:
Location: Taub 1
| 14:00 | Specification-Guided Learning of Nash Equilibria with High Social Welfare (abstract) PRESENTER: Kishor Jothimurugan |
| 14:20 | Synthesizing Fair Decision Trees via Iterative Constraint Solving (abstract) PRESENTER: Jingbo Wang |
| 14:40 | SMT-based Translation Validation for Machine Learning Compiler (abstract) PRESENTER: Juneyoung Lee |
| 15:00 | Verifying Fairness in Quantum Machine Learning (abstract) PRESENTER: Ji Guan |
| 15:20 | MoGym: Using Formal Models for Training and Verifying Decision-making Agents (abstract) PRESENTER: Maximilian Alexander Köhl |
15:30-16:00Coffee Break
16:00-17:30 Session 116A: Synthesis and Concurrency
Chair:
Location: Taub 1
| 16:00 | Synthesis and Analysis of Petri Nets from Causal Specifications (abstract) |
| 16:20 | Verifying generalised and structural soundness of workflow nets via relaxations (abstract) PRESENTER: Philip Offtermatt |
| 16:40 | Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET (abstract) PRESENTER: Andreas Katis |
| 16:50 | Information Flow Guided Synthesis (abstract) PRESENTER: Niklas Metzger |
| 17:10 | Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation (abstract) PRESENTER: Andreas Gittis |