Program

July 21st (Monday Workshops)

July 22nd (Tuesday Workshops)

July 23rd (Wednesday)

Time Room A Room B
8:30-9:00 Breakfast
9:00-10:30 Opening Remarks; CAV Award
10:30-11:00 Coffee break
11:00-12:00 Keynote
12:00-14:00 Lunch
14:00-15:30 Hardware Model Checking Probabilistic Reasoning I
15:30-16:00 Coffee break
16:00-17:30 Synthesis and Learning Concurrency and Runtime Verification
17:30-17:45
17:45-18:45 Industry Panel
19:00 Reception

11:00-12:00 Keynote

Room: TBD
11:00-12:00
Through the Looking Glass: Semantic Analysis of Neural Networks
Corina Păsăreanu, Carnegie Mellon University, USA

14:00-15:30 Hardware Model Checking

Room: A
Session Chair: TBD
14:00-14:20
Infinite-state Liveness Checking with rlive
Alessandro Cimatti, Alberto Griggio (Fondazione Bruno Kessler), Christopher Johannsen, Kristin Yvonne Rozier (Iowa State University), Stefano Tonetta (FBK)
14:20-14:40
Deeply Optimizing the SAT Solver for the IC3 Algorithm
Yuheng Su (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Qiusong Yang (Institute of Software, Chinese Academy of Sciences, Beijing, China); Yiwei Ci (Institute of Software, Chinese Academy of Sciences); Yingcheng Li, Tianjun Bu (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Ziyu Huang (Beijing Forestry University)
14:40-15:00
Property Directed Reachability with Extended Resolution
Yakir Vizel, Andrew Luka (Technion - Israel Institute of Technology)
15:00-15:20
Introducing Certificates to the Hardware Model Checking Competition
Nils Froleyks (JKU Linz), Emily Yu (Institute of Science and Technology Austria), Mathias Preiner (Stanford University), Armin Biere (University of Freiburg), Keijo Heljanko (University of Helsinki)
15:20-15:30
Btor2-Select: Machine Learning Based Algorithm Selection for Hardware Model Checking
Zhengyang Lu (University of Waterloo), Po-Chun Chien (LMU Munich), Nian-Ze Lee (National Taiwan University), Arie Gurfinkel (University of Waterloo), Vijay Ganesh (Georgia Institute of Technology)

14:00-15:30 Probabilistic Reasoning I

Room: B
Session Chair: TBD
14:00-14:20
Quantitative Supermartingale Certificates
Alessandro Abate (University of Oxford); Mirco Giacobbe, Diptarko Roy (University of Birmingham)
14:20-14:40
Supermartingale Certificates for Quantitative Omega-regular Verification and Control
Thomas A. Henzinger (IST Austria); Kaushik Mallik (IMDEA Software Institute); Pouya Sadeghi (University of Tehran); Djordje Zikelic (Singapore Management University)
14:40-15:00
Approximate Probabilistic Bisimulation for Continuous-Time Markov Chains
Timm Spork, Christel Baier (Technische Universität Dresden); Joost-Pieter Katoen (RWTH Aachen University); Sascha Klüppelholz (Technische Universität Dresden); Jakob Piribauer (Technische Universität Dresden; Universität Leipzig)
15:00-15:20
On the Almost-Sure Termination of Probabilistic Counter Programs
Sergei Novozhilov (Zhejiang University; The Hong Kong University of Science and Technology); Mingqi Yang, Mingshuai Chen, Zhiyang Li, Jianwei Yin (Zhejiang University)
15:20-15:30
POPACheck: A Model Checker for Probabilistic Pushdown Automata
Francesco Pontiggia, Ezio Bartocci, Michele Chiari (TU Wien)

16:00-17:30 Synthesis and Learning

Room: A
Session Chair: TBD
16:00-16:20
Deductive Synthesis of Reinforcement Learning Agents for Infinite Horizon Tasks
Yuning Wang, He Zhu (Rutgers)
16:20-16:40
Automata Learning from Preference and Equivalence Queries
Eric Hsiung, Joydeep Biswas, Swarat Chaudhuri (University of Texas at Austin)
16:40-17:00
Branching Bisimulation Learning
Alessandro Abate (University of Oxford); Mirco Giacobbe (University of Birmingham); Christian Micheletti (University of Padua); Yannik Schnitzer (University of Oxford)
17:00-17:10
Extending AALpy with Passive Learning: A Generalized State-Merging Approach
Benjamin von Berg, Bernhard Aichernig (TU Graz)
17:10-17:20
LearnLib: 10 years later
Markus Frohme (Technische Universität Dortmund); Falk Howar (Technische Universität Dortmund, Fraunhofer ISST); Bernhard Steffen (Technische Universität Dortmund)
17:20-17:30
A Misconception-Driven Adaptive Tutor for Linear Temporal Logic
Siddhartha Prasad (Brown University); Ben Greenman (University of Utah, USA); Tim Nelson, Shriram Krishnamurthi (Brown University)

16:00-17:30 Concurrency and Runtime Verification

Room: B
Session Chair: TBD
16:00-16:20
GPUMC: A Stateless Model Checker for GPU Weak Memory Concurrency
Soham Chakraborty (TU Delft); S. Krishna (IIT Bombay); Andreas Pavlogiannis (Aarhus University); Omkar Tuppe (IIT Bombay)
16:20-16:40
Counterexample-Guided Commutativity
Marcel Ebbinghaus, Dominik Klumpp, Andreas Podelski (University of Freiburg)
16:40-17:00
Scaling Up Proactive Enforcement
François Hublet (ETH Zürich); Leonardo Lima (University of Copenhagen); David Basin, Srdjan Krstic (ETH Zürich); Dmitriy Traytel (University of Copenhagen)
17:00-17:10
An Intermediate Program Representation for Optimizing Stream-Based Languages
Frederik Scheerer, Jan Baumeister, Bernd Finkbeiner, Arthur Correnson (CISPA Helmholtz Center for Information Security)
17:10-17:20
PyCaliper: Python-embedded Infrastructure for RTL Verification and Specification Synthesis
Adwait Godbole (University of California, Berkeley); Brian Huffman (Intel Labs); Fangfei Liu (Intel); Carlos V Rozas (Intel Labs); Sanjit A. Seshia (University of California, Berkeley)

July 24th (Thursday)

Time Room A Room B
8:30-9:00 Breakfast
9:00-10:30 Neural Networks Model Counting and First-Order Logic
10:30-11:00 Coffee break
11:00-12:00 Keynote
12:00-14:00 Lunch
14:00-15:30 Data Structures Reactive Synthesis
15:30-16:00 Coffee break
16:00-17:30 Cryptography and Security Model Checking
17:30-18:45
19:00 Banquet

9:00-10:30 Neural Networks

Room: A
Session Chair: TBD
9:00-9:20
Floating-Point Neural Networks Are Provably Robust Universal Approximators
Geonho Hwang (GIST); Wonyeol Lee (POSTECH); Yeachan Park (Sejong University); Sejun Park (Korea University); Feras Saad (Carnegie Mellon University)
9:20-9:40
A Formally Verified Robustness Certifier for Neural Networks
James Tobler (University of Queensland); Hira Taqdees Syeda, Toby Murray (University of Melbourne)
9:40-10:00
Policy Verification in Stochastic Dynamical Systems Using Logarithmic Neural Certificates
Thom Badings (University of Oxford); Wietze Koops (Lund University); Sebastian Junges (Radboud University); Nils Jansen (Ruhr-University Bochum)
10:00-10:10
StarV: A Qualitative and Quantitative Verification Tool for Learning-enabled Systems
Hoang-Dung Tran (University of Nebraska Lincoln); SungWoo Choi (University of Nebraska, Lincoln, School of Computing); Yuntao Li, Qing Liu (University of Nebraska-Lincoln); Hideki Okamoto (Toyota NA R&D); Bardh Hoxha (Toyota Research Institute North America); Georgios Fainekos (Toyota Motor North America)
10:10-10:20
ModelVerification.jl: a Comprehensive Toolbox for Formally Verifying Deep Neural Networks
Tianhao Wei, Hanjiang Hu (Carnegie Mellon University); Luca Marzari (University of Verona); Kai S. Yun, Peizhi Niu, Xusheng Luo, Changliu Liu (Carnegie Mellon University)
10:20-10:30
NeuralSAT: A High-Performance Verification Tool for Deep Neural Networks
Hai Duong, ThanhVu (Vu) Nguyen (George Mason University); Matthew B Dwyer (University of Virginia)

9:00-10:30 Model Counting and First-Order Logic

Room: B
Session Chair: TBD
9:00-9:20
Polyregular Model Checking
Aliaume Lopez, Rafał Stefański (University of Warsaw)
9:20-9:40
Engineering an Efficient Probabilistic Exact Model Counter
Mate Soos (University of Toronto); Kuldeep S. Meel (Georgia Institute of Technology and University of Toronto)
9:40-9:50
Decision Heuristics in MCSat
Thomas Hader (TU Wien); Ahmed Irfan, Stephane Graham-Lengrand (SRI International)
9:50-10:00
Veil: A Framework for Automated and Interactive Verification of Transition Systems
George Pîrlea, Vladimir Gladshtein (National University of Singapore); Elad Kinsbruner (Technion); Qiyuan Zhao, Ilya Sergey (National University of Singapore)
10:00-10:10
The Vampire Diary
Filip Bartek (Czech Technical University in Prague); Ahmed Bhayat (University of Manchester); Robin Coutelier, Marton Hajdu, Matthias Hetzenberger (TU Wien); Petra Hozzova (Czech Technical University in Prague); Laura Kovacs, Jakob Rath (TU Wien); Michael Rawson (University of Southampton); Giles Reger (The University of Manchester); Martin Suda (Czech Technical University in Prague); Johannes Schoisswohl (TU Wien); Andrei Voronkov (The University of Manchester)
10:10-10:20
Panini: An Efficient and Flexible Knowledge Compiler
Yong Lai (Jilin Univeristy); Kuldeep S. Meel (Georgia Institute of Technology); Roland H. C. Yap (National University of Singapore)

11:00-12:00 Keynote

Room: TBD
11:00-12:00
Side Channel Secure Software: A Hardware Question
Roderick Bloem, Graz University of Technology, Austria

14:00-15:30 Data Structures

Room: A
Session Chair: TBD
14:00-14:20
Verifying Tree-Manipulating Programs via CHCs
Marco Faella (University of Naples Federico II); Gennaro Parlato (University of Molise)
14:20-14:40
Automated Verification of Monotonic Data Structure Traversals in C
Matthew Sotoudeh (Stanford University)
14:40-15:00
Arithmetizing Shape Analysis
Sebastian Wolff, Ekanshdeep Gupta (New York University); Zafer Esen (Uppsala University); Hossein Hojjat (TeIAS, Khatam University); Philipp Rümmer (University of Regensburg); Thomas Wies (New York University)
15:00-15:20
Raven: An SMT-Based Concurrency Verifier
Ekanshdeep Gupta, Nisarg Patel, Thomas Wies (New York University)
15:20-15:30
Fifteen Years of Viper
Marco Eilers, Malte Schwerhoff (ETH Zurich); Alexander J. Summers (University of British Columbia); Peter Müller (ETH Zurich)

14:00-15:30 Reactive Synthesis

Room: B
Session Chair: TBD
14:00-14:20
Scaling GR(1) Synthesis via a Compositional Framework for LTL Discrete Event Control
Hernán Gabriel Gagliardi (Universidad de Buenos Aires); Victor Braberman (Universidad de Buenos Aires/CONICET); Sebastian Uchitel (Universidad de Buenos Aires, CONICET, Imperial College London)
14:20-14:40
Counter Example Guided Reactive Synthesis for LTL Modulo Theories
Andoni Rodriguez (IMDEA Software Institute and Universidad Politecnica de Madrid, Spain); Felipe Gorostiaga, Cesar Sanchez (IMDEA Software Institute)
14:40-15:00
Automatic Synthesis of Smooth Infinite Horizon Paths Satisfying Linear Temporal Logic Specifications
Samuel Williams, Jyotirmoy Deshmukh (University of Southern California)
15:00-15:20
Full LTL Synthesis over Infinite-state Arenas
Shaun Azzopardi (N/A); Luca Di Stefano (TU Wien); Nir Piterman, Gerardo Schneider (University of Gothenburg and Chalmers University of Technology)
15:20-15:30
Issy: A Comprehensive Tool for Specification and Synthesis of Infinite-State Reactive Systems
Philippe Heim, Rayna Dimitrova (CISPA Helmholtz Center for Information Security)

16:00-17:30 Cryptography and Security

Room: A
Session Chair: TBD
16:00-16:20
Automated Verification of Consistency in Zero-Knowledge Proof Circuits
Jon Stephens (University of Texas at Austin); Shankara Pailoor (Veridise Inc); Isil Dillig (University of Texas at Austin)
16:20-16:40
Integer Reasoning Modulo Different Constants in SMT
Elizaveta Pertseva, Alex Ozdemir (Stanford); Shankara Pailoor, Alp Bassa (Veridise); Sorawee Porncharoenwase (Amazon); Işil Dillig (UT Austin); Clark Barrett (Stanford)
16:40-17:00
Structural operational semantics for functional and security verification of pipelined processors
Robert Colvin (University of Queensland); Roger Su (Australian National University)
17:00-17:20
Relational Hoare Logic for Realistically Modelled Machine Code
Denis Mazzucato (Carnegie Mellon University); Abdalrhman Mohamed (Stanford University); Juneyoung Lee (Amazon Web Services); Clark Barrett (Stanford University); Jim Grundy, John Harrison (Amazon Web Services); Corina Pasareanu (NASA Ames and Carnegie Mellon University)

16:00-17:30 Model Checking

Room: B
Session Chair: TBD
16:00-16:20
Efficient Probabilistic Model Checking for Relational Reachability
Lina Gerlach (RWTH Aachen Univsersity); Tobias Winkler, Erika Ábrahám (RWTH Aachen University); Borzoo Bonakdarpour (Michigan State University); Sebastian Junges (Radboud University)
16:20-16:30
Verifying PETSc Vector Components Using CIVL
Venkata Narayana Sarma Dhavala, Stephen F. Siegel (University of Delaware); Jan Hueckelheim, Paul Hovland (Argonne National Laboratory)
16:30-16:50
Compositional Abstraction for Timed Systems with Broadcast Synchronization
Hanyue Chen (Tongji University); Miaomiao Zhang (Tongji Uniersity); Frits Vaandrager (Radboud University)
16:50-17:00
The rIC3 Hardware Model Checker
Yuheng Su (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Qiusong Yang, Yiwei Ci (Institute of Software, Chinese Academy of Sciences, Beijing, China); Tianjun Bu (University of Chinese Academy of Sciences; Institute of Software, Chinese Academy of Sciences); Ziyu Huang (Beijing Forestry University)
17:00-17:10
HornStr: Invariant Synthesis for Regular Model Checking as Constrained Horn Clauses
Hongjian Jiang, Anthony W. Lin (RPTU and MPI-SWS); Oliver Markgraf (RPTU); Philipp Rümmer (University of Regensburg); Daniel Stan (LRE, Epita)

July 25th (Friday)

Time Room A Room B
8:30-9:00 Breakfast
9:00-10:30 Decision Procedures MDPs and Probabilistic Reasoning
10:30-11:00 Coffee break
11:00-12:00 Keynote
12:00-14:00 Lunch, Logic Lounge
14:30-15:30 Quantum Computing Probabilistic Reasoning II
15:30-16:00 Coffee break
16:00-17:30 Applications Networks and Protocols
17:30-17:45
17:45-18:45 Business Meeting

9:00-10:30 Decision Procedures

Room: A
Session Chair: TBD
9:00-9:20
Regex Decision Procedures in Extended RE#
Ian Erik Varatalu (Tallinn University of Technology); Margus Veanes (MSR Redmond); Ekaterina Zhuchko, Juhan Ernits (Tallinn University of Technology)
9:20-9:40
Verified and Optimized Implementation of Orthologic Proof Search
Simon Guilloud, Clément Pit-Claudel (EPFL)
9:40-10:00
Accelerating Automated Program Verifiers by Automatic Proof Localization
Kiran Gopinathan (University of Illinois Urbana-Champaign); Dionysios Spiliopoulos (ETH Zurich); Vikram Goyal (National University of Singapore); Peter Müller, Markus Püschel (ETH Zurich); Ilya Sergey (National University of Singapore)
10:00-10:20
Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
Yicheng Qian (Stanford University); Joshua Clune (Carnegie Mellon University); Clark Barrett (Stanford University); Jeremy Avigad (Carnegie Mellon University)
10:20-10:30
Lean-SMT: An SMT tactic for discharging proof goals in Lean
Abdalrhman Mohamed (Stanford University); Tomaz Mascarenhas (Universidade Federal de Minas Gerais); Harun Khan (Stanford University); Haniel Barbosa (Universidade Federal de Minas Gerais); Andrew Reynolds (The University of Iowa, Amazon Web Services); Yicheng Qian (Stanford University); Cesare Tinelli (The University of Iowa); Clark Barrett (Stanford University)

9:00-10:30 MDPs and Probabilistic Reasoning

Room: B
Session Chair: TBD
9:00-9:20
A Formally Verified IEEE 754 Floating-Point Implementation of Interval Iteration for MDPs
Bram Kohlen (University of Twente); Maximilian Schäffeler (TU Munich); Mohammad Abdulaziz (King's College London); Arnd Hartmanns, Peter Lammich (University of Twente)
9:20-9:40
INTERLEAVE: A Faster Symbolic Algorithm for Maximal End Component Decomposition
Suguman Bansal (Georgia Institute of Technolgy); Ramneet Singh (Indian Institute of Technology Delhi)
9:40-10:00
Small Decision Trees for MDPs with Deductive Synthesis
Roman Andriushchenko, Milan Češka (Brno University of Technology); Sebastian Junges (Radboud University); Filip Macák (Brno University of Technology)
10:00-10:20
Approximating Fixpoints of Approximated Functions
Paolo Baldan (University of Padova); Sebastian Gurke (University of Duisburg-Essen, Germany); Barbara König (University of Duisburg-Essen); Tommaso Padoan (Università di Trieste); Florian Wittbold (University of Duisburg-Essen)
10:20-10:30
StatWhy: Formal Verification Tool for Statistical Hypothesis Testing Programs
Yusuke Kawamoto (AIST); Kentaro Kobayashi (Tsukuba University & AIST); Kohei Suenaga (Kyoto University)

11:00-12:00 Keynote

Room: TBD
11:00-12:00
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization
Emina Torlak, AWS and University of Washington, USA

14:30-15:30 Quantum Computing

Room: A
Session Chair: TBD
14:30-14:50
Verifying Fault-Tolerance of Quantum Error Correction Codes
Kean Chen, Yuhao Liu (University of Pennsylvania); Wang Fang (University of Edinburgh); Jennifer Paykin, Xin-Chuan Wu, Albert Schmitz (Intel Corporation); Steve Zdancewic, Gushu Li (University of Pennsylvania)
14:50-15:10
FeynmanDD: Quantum Circuit Analysis with Classical Decision Diagrams
Ziyuan Wang (Tsinghua); Bin Cheng (NUS); Longxiang Yuan (Tsinghua); Zhengfeng Ji (Tsinghua and Zhongguancun Lab)
15:10-15:30
D-Hammer: Efficient Equational Reasoning for Labelled Dirac Notation
Yingte Xu (Max Planck Institute for Security and Privacy); Gilles Barthe (Max Planck Institute for Security and Privacy & IMDEA Software Institute); Li Zhou (Institute of Software, Chinese Academy of Sciences)

14:30-15:30 Probabilistic Reasoning II

Room: B
Session Chair: TBD
14:30-14:50
Assessing the Quality of Binomial Samplers: A Statistical Distance Framework
Sourav Chakraborty (Indian Statistical Institute); Kuldeep S. Meel (Georgia Institute of Technology); Uddalok Sarkar (Indian Statistical Institute)
14:50-15:10
Robust Probabilistic Bisimilarity for Labelled Markov Chains
Franck van Breugel (York University); Syyeda Zainab Fatmi, Stefan Kiefer, David Parker (University of Oxford)
15:10-15:30
Accelerating Markov Chain Model Checking: Good-for-Games Meets Unambiguous Automata Specifications
Yong Li (Institute of Software, Chinese Academy of Sciences); Soumyajit Paul, Sven Schewe, Qiyi Tang (University of Liverpool)

16:00-17:30 Applications

Room: A
Session Chair: TBD
16:00-16:20
On the Complexity of Checking Mixed Isolation Levels for SQL Transactions
Ahmed Bouajjani (IRIF, CNRS, University Paris Cité); Constantin Enea (LIX, École Polytechnique, CNRS and Institut Polytechnique de Paris); Enrique Román-Calvo (IRIF, CNRS, University Paris Cité)
16:20-16:40
Data-driven Verification of Procedural Programs with Integer Arrays
Ahmed Bouajjani (Université Paris Cité); Wael-Amine Boutglay (Université Paris Cité and Mohammed VI Polytechnic University); Peter Habermehl (Université Paris Cité)
16:40-16:50
Automated Parameterized Verification of a Railway Protection System with Dafny
Roberto Cavada, Alessandro Cimatti, Alberto Griggio, Christian Lidström, Gianluca Redondi (Fondazione Bruno Kessler); Giuseppe Scaglione, Matteo Tessi (RFI); Dylan Trenti (Fondazione Bruno Kessler)
16:50-17:00
Charon: An Analysis Framework for Rust
Son Ho (Inria, Microsoft Azure Research); Guillaume Boisseau (Inria); Lucas Franceschino (Cryspen); Yoann Prak, Aymeric Fromherz (Inria); Jonathan Protzenko (Microsoft Azure Research)
17:00-17:10
Surfer – An Extensible Waveform Viewer
Frans Skarman (Linköping University); Lucas Klemmer, Daniel Große (Johannes Kepler University); Oscar Gustafsson (Linköping University); Kevin Laeufer (Cornell University)
17:10-17:20
PyEuclid: A Versatile Formal Plane Geometry System in Python
Zhaoyu Li, Hangrui Bi, Jialiang Sun (University of Toronto); Zenan Li (Nanjing University); Kaiyu Yang (Meta FAIR); Xujie Si (University of Toronto)

16:00-17:30 Networks and Protocols

Room: B
Session Chair: TBD
16:00-16:20
Automatic Verification of Floating-Point Accumulation Networks
David K. Zhang, Alex Aiken (Stanford University)
16:20-16:40
Counting Abstraction and Decidability for the Verification of Structured Parameterized Networks
Marius Bozga, Radu Iosif (Univ. Grenoble Alpes, Grenoble INP, VERIMAG); Arnaud Sangnier (DIBRIS, Univ. of Genova, Italy); Neven Villani (Univ. Grenoble Alpes, Grenoble INP, VERIMAG)
16:40-17:00
QSM-Cutoff: Systematic Derivation of Quantified Cutoff Formulas for Distributed Protocols
Yun-Rong Luo (University of Michigan, Ann Arbor); Aman Goel (AWS); Karem Sakallah (University of Michigan)
17:00-17:10
Space Explanations of Neural Network Classification
Faezeh Labbaf, Tomas Kolarik (University of Lugano (USI)); Martin Blicha (University of Lugano (USI), Ethereum Foundation) Grigory Fedyukovich (Florida State University, University of Lugano (USI)); Michael Wand (SUPSI, IDSIA, Lugano); Natasha Sharygina (University of Lugano (USI))
17:10-17:20
SPROUT: A Verifier for Symbolic Multiparty Protocols
Elaine Li (New York University); Felix Stutz (University of Luxembourg); Thomas Wies (New York University); Damien Zufferey (NVIDIA)