Session: Decision Procedures 1

Chair: Anthony Lin

11:00

Satisfiability Modulo Finite Fields

Alex Ozdemir (Stanford University), Gereon Kremer (Stanford University, Certora), Clark Barrett (Stanford University), Cesare Tinelli (The University of Iowa)

11:20

Exploiting Adjoints in Property Directed Reachability Analysis

Mayuko Kori (National Institute of Informatics), Flavio Ascari (University of Pisa), Filippo Bonchi (University of Pisa), Roberto Bruni (University of Pisa), Roberta Gori (University of Pisa), Ichiro Hasuo (National Institute of Informatics)

Distinguished Paper

11:40

Fast Approximations of Quantifier Elimination

Isabel Garcia-Contreras (University of Waterloo), Hari Govind V K (University of Waterloo), Sharon Shoham (Tel Aviv University), Arie Gurfinkel (University of Waterloo)

Distinguished Paper

Session: Software Verification 1

Chair: Serdar Tasiran

2:00

Formula Normalizations in Verification

Simon Guilloud (EPFL), Mario Bucev (EPFL), Dragana Milovancevic (EPFL), Viktor Kunčak (EPFL)

2:20

Automatic Program Instrumentation for Automatic Verification

Jesper Amilon (KTH Royal Institute of Technology), Zafer Esen (Uppsala University), Dilian Gurov (KTH Royal Institute of Technology), Christian Lidström (KTH Royal Institute of Technology), Philipp Rümmer (University of Regensburg)

Distinguished Paper

2:40

Automated Verification of Correctness for Masked Arithmetic Programs

Mingyang Liu (ShanghaiTech University), Fu Song (ShanghaiTech University), Taolue Chen (Birkbeck, University of London)

3:00

Boolean Abstractions for Realizability Modulo Theories

Andoni Rodriguez (IMDEA Software Institute), Cesar Sanchez (IMDEA Software Institute)

3:20

Kratos2: an SMT-Based Model Checker for Imperative Programs [Tool Paper]

Alberto Griggio (Fondazione Bruno Kessler), Martin Jonáš (Masaryk University, Czech Republic)

Session: Probabilistic systems

Chair: Kuldeep Meel

4:00

A Flexible Toolchain for Symbolic Rabin Games under Fairness and Stochastic Uncertainties [Tool Paper]

Rupak Majumdar (MPI-SWS), Kaushik Mallik (ISTA), Mateusz Rychlicki (University of Leeds), Anne-Kathrin Schmuck (Max Planck Institute for Software Systems), Sadegh Soudjani (Newcastle University)

4:10

Efficient Sensitivity Analysis for Parametric Robust Markov Chains

Thom Badings (Radboud University), Sebastian Junges (Radboud University), Ahmadreza Marandi (Eindhoven University of Technology), Ufuk Topcu (The University of Texas at Austin), Nils Jansen (Radboud University)

4:30

Compositional Probabilistic Model Checking with String Diagrams of MDPs

Kazuki Watanabe (The Graduate University for Advanced Studies (SOKENDAI)), Clovis Eberhart (National Institute of Informatics), Kazuyuki Asada (Tohoku University), Ichiro Hasuo (National Institute of Informatics)

4:50

Automated Tail Bound Analysis for Probabilistic Recurrence Relations

Yican Sun (Peking University), Hongfei Fu (Shanghai Jiao Tong University), Krishnendu Chatterjee (IST Austria), Amir Kafshdar Goharshady (Hong Kong University of Science and Technology)

5:10

Search and Explore: Symbiotic Policy Synthesis in POMDPs

Roman Andriushchenko (Brno University of Technology, Czech Republic), Alexander Bork (RWTH-Aachen University, Germany), Milan Ceska (Brno University of Technology, Czech Republic), Sebastian Junges (Radboud University, Netherlands), Joost-Pieter Katoen (RWTH-Aachen University, Germany), Filip Macak (Brno University of Technology, Czech Republic)

5:30

MDPs as Distribution Transformers: Affine Invariant Synthesis for Safety Objectives

S. Akshay (IIT Bombay), Krishnendu Chatterjee (Institute of Science and Technology Austria (ISTA)), Tobias Meggendorfer (Institute of Science and Technology Austria (ISTA)), Đorđe Žikelić (Institute of Science and Technology Austria (ISTA))

Session: Software Verification 1.5

Chair: Kuldeep Meel

5:50

Ownership guided C to Rust translation

Hanliang Zhang (University of Bristol), Cristina David (University of Bristol), Yijun Yu (The Open University), Meng Wang (University of Bristol)

Session: Neural Networks and Machine Learning

Chair: Pavithra Prabhakar

9:00

Verifying Generalization in Deep Learning [Case Study]

Guy Amir (The Hebrew University of Jerusalem), Osher Maayan (The Hebrew University of Jerusalem), Tom Zelazny (The Hebrew University of Jerusalem), Guy Katz (The Hebrew University of Jerusalem), Michael Schapira (The Hebrew University of Jerusalem)

9:10

Monitoring Algorithmic Fairness

Thomas A. Henzinger (Instititue of Science and Technology Austria), Mahyar Karimi (University of Tehran), Konstantin Kueffner (Instititue of Science and Technology Austria), Kaushik Mallik (Instititue of Science and Technology Austria)

9:30

QEBVerif: Quantization Error Bound Verification of Neural Networks

Yedi Zhang (Shanghaitech University), Fu Song (ShanghaiTech University), Jun Sun (Singapore Management University)

9:50

Certifying the Fairness of KNN in the Presence of Dataset Bias

Yannan Li (University of Southern California), Jingbo Wang (University of Southern California), Chao Wang (University of Southern California)

10:10

NNV 2.0: The Neural Network Verification Tool [Tool Paper]

Diego Manzanas Lopez (Vanderbilt University), Sung Woo Choi (University of Nebraska), Hoang Dung Tran (University of Nebraska), Taylor T. Johnson (Vanderbilt University)

10:20

nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models [Tool Paper]

Matthias Cosler (CISPA Helmholtz Center for Information Security), Christopher Hahn (Stanford University), Daniel Mendoza (Stanford University), Frederik Schmitt (CISPA Helmholtz Center for Information Security), Caroline Trippel (Stanford University)

Session: Security and Quantum Systems

Chair: Sébastien Bardin

2:00

Symbolic Quantum Simulation with Quasimodo [Tool Paper]

Meghana Sistla (The University of Texas at Austin), Swarat Chaudhuri (UT Austin), Thomas Reps (University of Wisconsin)

2:10

AutoQ: An Automata-based Quantum Circuit Verifier [Tool Paper]

Yu-Fang Chen (Academia Sinica), Kai-Min Chung (Academia Sinica), Ondřej Lengál (Brno University of Technology), Jyun-Ao Lin (Academia Sinica), Wei-Lun Tsai (Academia Sinica)

2:20

Formally Verified EVM Block-Optimizations [Tool Paper]

Elvira Albert (Universidad Complutense de Madrid), Samir Genaim (Universidad Complutense de Madrid), Daniel Kirchner (Ethereum Foundation & University of Bamberg), Enrique Martin-Martin (Universidad Complutense de Madrid)

2:30

Verifying the Verifier: eBPF Range Analysis Verification

Harishankar Vishwanathan (Rutgers University), Matan Shachnai (Rutgers University), Srinivas Narayana (Rutgers University), Santosh Nagarakatte (Rutgers University)

2:50

Bounded Verification for Finite-Field-Blasting (in a Compiler for Zero Knowledge Proofs)

Alex Ozdemir (Stanford University), Riad Wahby (Carnegie Mellon University), Fraser Brown (Carnegie Mellon University), Clark Barrett (Stanford University)

3:10

SR-SFLL: Structurally Robust Stripped Functionality Logic Locking

Gourav Takhar (Indian Institute of Technology Kanpur), Subhajit Roy (Indian Institute of Technology Kanpur)

Session: Decision Procedures 2

Chair: Mihaela Sighireanu

4:00

Solving String Constraints using SAT

Kevin Lotz (Kiel University), Amit Goel (AWS), Bruno Dutertre (AWS), Benjamin Kiesl-Reiter (AWS), Soonho Kong (AWS), Rupak Majumdar (AWS), Dirk Nowotka (Kiel University)

4:20

Rounding Meets Approximate Model Counting

Jiong Yang (National University of Singapore), Kuldeep S. Meel (National University of Singapore)

Distinguished Paper

4:40

Partial Quantifier Elimination And Property Generation

Eugene Goldberg (None)

5:00

Decision Procedures for Sequence Theories

Artur Jeż (University of Wroclaw), Anthony Lin (Technische Universität Kaiserslautern and Max-Planck Institute for Software Systems), Oliver Markgraf (Technische Universität Kaiserslautern), Philipp Ruemmer (University of Regensburg)

5:20

Local Search for Solving Satisfiability of Polynomial Formulas

Haokun Li (Peking University), Bican Xia (Peking University), Tianqi Zhao (Peking University)

5:40

The Golem Horn Solver [Tool Paper]

Martin Blicha (Università della Svizzera italiana), Konstantin Britikov (Università della Svizzera italiana), Natasha Sharygina (Università della Svizzera italiana)

Distinguished Paper

5:50

Bitwuzla [Tool Paper]

Aina Niemetz (Stanford University), Mathias Preiner (Stanford University)

Distinguished Paper

Session: Cyber-physical and Hybrid Systems

Chair: Ichiro Hasuo

9:00

Closed-loop Analysis of Vision-based Autonomous Systems: A Case Study [Case Study]

Corina Pasareanu (KBR Inc., NASA Ames, Carnegie Mellon University), Ravi Mangal (Carnegie Mellon University), Divya Gopinath (KBR Inc., NASA Ames), Sinem Getir Yaman (University of York), Calum Imrie (University of York), Radu Calinescu (University of York), Huafeng Yu (Boeing Research and Technology)

9:10

Hybrid Controller Synthesis for Nonlinear Systems Subject to Reach-avoid Constraints

Zhengfeng Yang (East China Normal University), Li Zhang (East China Normal University), Xia Zeng (Southwest University), Xiaochao Tang (East China Normal University), Chao Peng (East China Normal University), Zhenbing Zeng (Shanghai University)

9:30

Safe Environmental Envelopes of Discrete Systems

Romulo Meira-Goes (Pennsylvania State University), Ian Dardik (Carnegie Mellon University), Eunsuk Kang (Carnegie Mellon University), Stéphane Lafortune (University of Michigan, Ann Arbor), Stavros Tripakis (Northeastern University)

9:50

A Unified Model for Real-Time Systems: Symbolic Techniques and Implementation

S. Akshay (Indian Institute of Technology Bombay), Paul Gastin (Université Paris-Saclay, ENS Paris-Saclay, CNRS), R Govind (Indian Institute of Technology Bombay), Aniruddha Joshi (Indian Institute of Technology Bombay), B Srivathsan (Chennai Mathematical Institute, India)

10:10

Verse: A Python library for reasoning about multi-agent hybrid system scenarios [Tool Paper]

Yangge Li (University of Illinois at Urbana-Champaign), Haoqing Zhu (University of Illinois at Urbana-Champaign), Katherine Braught (University of Illinois at Urbana-Champaign), Keyi Shen (University of Illinois at Urbana-Champaign), Sayan Mitra (University of Illinois at Urbana-Champaign)

10:20

3D Environment Modeling for Falsification and Beyond with Scenic 3.0 [Tool Paper]

Eric Vin (University of California, Santa Cruz), Shun Kashiwa (University of California, Santa Cruz), Matthew Rhea (SentinelOne), Daniel J. Fremont (University of California, Santa Cruz), Edward Kim (University of California, Berkeley), Tommaso Dreossi (insitro), Shromona Ghosh (Waymo LLC), Xiangyu Yue (The Chinese University of Hong Kong), Alberto L. Sangiovanni-Vincentelli (University of California, Berkeley), Sanjit A. Seshia (University of California, Berkeley)

Session: Model checking

Chair: Elizabeth Polgreen

2:00

Model Checking Race-freedom When “Sequential Consistency for Data-race-free Programs” is Guaranteed

Wenhao Wu (University of Delaware), Jan Hueckelheim (Argonne National Laboratory), Paul Hovland (Argonne National Laboratory), Ziqing Luo (University of Delaware), Stephen F. Siegel (University of Delaware)

2:20

Incremental Dead State Detection in Logarithmic Time

Caleb Stanford (UC San Diego and UC Davis), Margus Veanes (MSR Redmond)

2:40

Searching for i-Good Lemmas to Accelerate Safety Model Checking

Yechuan Xia (East China Normal University), Anna Becchi (Fondazione Bruno Kessler), Alessandro Cimatti (FBK), Alberto Griggio (Fondazione Bruno Kessler), Jianwen Li (East China Normal University), Geguang Pu (East China Normal University)

3:00

Second-Order Hyperproperties

Raven Beutner (CISPA Helmholtz Center for Information Security, Germany), Bernd Finkbeiner (CISPA Helmholtz Center for Information Security), Hadar Frenkel (CISPA Helmholtz Center for Information Security), Niklas Metzger (CISPA Helmholtz Center for Information Security)

3:20

CoqCryptoLine: A Verified Model Checker with Certified Results [Tool Paper]

Ming-Hsien Tsai (National Institute of Cyber Security), Yu-Fu Fu (Georgia Institute of Technology), Jiaxiang Liu (Shenzhen University), Xiaomu Shi (Shenzhen University), Bow-Yaw Wang (Academia Sinica), Bo-Yin Yang (Academia Sinica)

Session: Concurrency

Chair: Ahmed Bouajjani

4:00

nekton: a linearizability proof checker [Tool Paper]

Roland Meyer (TU Braunschweig), Anton Opaterny (TU Braunschweig), Thomas Wies (New York University), Sebastian Wolff (New York University)

4:10

Lincheck: A Practical Framework for Testing Concurrent Data Structures on JVM [Tool Paper]

Nikita Koval (JetBrains), Alexander Fedorov (IST Austria), Maria Sokolova (JetBrains), Dmitry Tsitelov (Devexperts), Dan Alistarh (IST Austria)

4:20

Fast Termination and Workflow Nets

Philip Offtermatt (Université de Sherbrooke & University of Warsaw), Filip Mazowiecki (University of Warsaw), Piotr Hofman (University of Warsaw)

4:40

Rely-Guarantee Reasoning for Causally Consistent Shared Memory

Ori Lahav (Tel Aviv University), Brijesh Dongol (University of Surrey), Heike Wehrheim (University of Oldenburg)

5:00

Overcoming Memory Weakness with Unified Fairness

Parosh Aziz Abdulla (Uppsala University), Mohamed Faouzi Atig (Uppsala University), Adwait Godbole (University of California, Berkeley), Shankaranarayanan Krishna (IIT Bombay), Mihir Vahanwala (MPI-SWS, Saarbrücken)

5:20

Unblocking Dynamic Partial Order Reduction

Michalis Kokologiannakis (MPI-SWS), Iason Marmanis (MPI-SWS), Viktor Vafeiadis (MPI-SWS)

5:40

Commutativity For Concurrent Program Termination Proofs

Azadeh Farzan (University of Toronto), Danya Lette (University of Toronto)

Session: Automata and Logic

Chair: Bernd Finkbeiner

9:00

Online Causation Monitoring of Signal Temporal Logic

Zhenya Zhang (Kyushu University), Jie An (National Institute of Informatics), Paolo Arcaini (National Institute of Informatics), Ichiro Hasuo (National Institute of Informatics)

9:20

Learning Assumptions for Compositional Verification of Timed Automata

Hanyue Chen (Tongji University), Yu Su (Tongji University), Miaomiao Zhang (Tongji University), Zhiming Liu (Southwest University), Junri Mi (Tongji University)

9:40

Active Learning of Deterministic Timed Automata with Myhill-Nerode Style Characterization

Masaki Waga (Kyoto University)

10:00

Process Equivalence Problems as Energy Games

Benjamin Bisping (TU Berlin)

10:20

Automated Analyses of IOT Event Monitoring Systems [Case study]

Andrew Apicelli (Amazon Web Services, Inc.), Sam Bayless (Amazon Web Services, Inc.), Ankush Das (Amazon Web Services, Inc.), Andrew Gacek (Amazon Web Services, Inc.), Dhiva Jaganathan (Amazon Web Services, Inc.), Saswat Padhi (Google LLC), Vaibhav Sharma (Amazon.com Services LLC), Michael W. Whalen (Amazon Web Services, Inc.), Raveesh Yadav (Amazon Web Services, Inc.)

Session: Synthesis 1

Chair: Bettina Könighofer

12:00

SYNTCOMP Report

12:10

Counter-Example Guided Knowledge Compilation for Boolean Functional Synthesis

S. Akshay (IIT Bombay), Supratik Chakraborty (IIT Bombay), Sahil Jain (IIT Bombay)

Session: Synthesis 2

Chair: Bettina Könighofer

2:00

Policy Synthesis and Reinforcement Learning for Discounted LTL

Rajeev Alur (University Of Pennsylvania), Osbert Bastani (University of Pennsylvania), Kishor Jothimurugan (University of Pennsylvania), Mateo Perez (University of Colorado Boulder), Fabio Somenzi (University of Colorado Boulder), Ashutosh Trivedi (University of Colorado Boulder)

2:20

Guessing Winning Policies in LTL Synthesis by Semantic Learning

Jan Kretinsky (Technische Universität München), Max Prokop (Technische Universität München), Tobias Meggendorfer (Institute of Science and Technology Austria), Sabine Rieder (Technische Universität München)

2:40

Synthesizing Trajectory Queries from Examples

Stephen Mell (University of Pennsylvania), Favyen Bastani (Allen Institute for AI), Steve Zdancewic (University of Pennsylvania), Osbert Bastani (University of Pennsylvania)

3:00

Synthesizing Permissive Winning Strategy Templates for Parity Games

Ashwani Anand (Max Planck Institute for Software Systems), Satya Prakash Nayak (Max Planck Institute for Software Systems), Anne-Kathrin Schmuck (Max Planck Institute for Software Systems)

Session: Software Verification 2

Chair: Zhilin Wu

4:00

Complete Multiparty Session Type Projection with Automata

Elaine Li (New York University), Felix Stutz (MPI-SWS), Thomas Wies (New York University), Damien Zufferey (Sonar Source)

4:20

Certified Verification for Algebraic Abstraction

Ming-Hsien Tsai (National Institute of Cyber Security), Yu-Fu Fu (Georgia Institute of Technology), Jiaxiang Liu (Shenzhen University), Xiaomu Shi (Shenzhen University), Bow-Yaw Wang (Academia Sinica), Bo-Yin Yang (Academia Sinica)

4:40

Early Verification of Legal Compliance via Bounded Satisfiability Checking

Nick Feng (University of Toronto), Lina Marsso (University of Toronto), Mehrdad Sabetzadeh (EECS, University of Ottawa), Marsha Chechik (University of Toronto)

5:00

Making IP=PSPACE Practical: Efficient Interactive Protocols for BDD Algorithms

Eszter Couillard (Technische Universität München), Philipp Czerner (Technische Universität München), Javier Esparza (Technische Universität München), Rupak Majumdar (Max Planck Institute for Software Systems)

5:20

R2U2 Version 3.0: Re-imagining a Toolchain for Specification, Resource Estimation, and Optimized Observer Generation for Runtime Verification in Hardware and Software [Tool Paper]

Chris Johannsen (Iowa State University), Phillip Jones (Iowa State University), Brian Kempa (Iowa State University), Kristin Yvonne Rozier (Iowa State University), Pei Zhang (Google)