| Authors | Title | Paper | Talk |
|---|
| Neha Rungta | A Billion SMT Queries a Day |  | |
| Arie Gurfinkel | Program Verification with Constrained Horn Clauses (Invited Paper) | | |
| Jialu Bao, Nitesh Trivedi, Drashti Pathak, Justin Hsu and Subhajit Roy | Data-Driven Invariant Learning for Probabilistic Programs | | Aug 07 09:00 |
| Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer and Đorđe Žikelić | Sound and Complete Certificates for Quantitative Termination Analysis of Probabilistic Programs | | Aug 07 09:20 |
| Mingshuai Chen, Joost-Pieter Katoen, Lutz Klinkenberg and Tobias Winkler | Does a Program Yield the Right Distribution? Verifying Probabilistic Programs via Generating Functions | | Aug 07 09:40 |
| Sebastian Junges and Matthijs T. J. Spaan | Abstraction-Refinement for Hierarchical Probabilistic Models | | Aug 07 10:00 |
| Marc Fischer, Christian Sprecher, Dimitar I. Dimitrov, Gagandeep Singh and Martin Vechev | Shared Certificates for Neural Network Verification | | Aug 07 14:00 |
| Brandon Paulsen and Chao Wang | Example Guided Synthesis of Linear Approximations for Neural Network Verification | | Aug 07 14:20 |
| Long H. Pham and Jun Sun | Verifying Neural Networks Against Backdoor Attacks | | Aug 07 14:40 |
| Peng Jin, Jiaxu Tian, Dapeng Zhi, Xuejun Wen and Min Zhang | Trainify: A CEGAR-Driven Training and Verification Framework for Safe Deep Reinforcement Learning | | Aug 07 15:00 |
| Marco Casadio, Ekaterina Komendantskaya, Matthew L. Daggitt, Wen Kokke, Guy Katz, Guy Amir and Idan Refaeli | Neural Network Robustness as a Verification Property: A Principled Case Study | | Aug 07 15:20 |
| Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata, Kohei Suenaga and Ichiro Hasuo | The Lattice-Theoretic Essence of Property Directed Reachability Analysis | | Aug 07 16:00 |
| Yucheng Ji, Hongfei Fu, Bin Fang and Haibo Chen | Affine Loop Invariant Generation via Matrix Algebra | | Aug 07 16:20 |
| Ahmed Bouajjani, Wael-Amine Boutglay and Peter Habermehl | Data-driven Numerical Invariant Synthesis with Automatic Generation of Attributes | | Aug 07 16:40 |
| Prantik Chatterjee, Jaydeepsinh Meda, Akash Lal and Subhajit Roy | Proof-guided Underapproximation Widening for Bounded Model Checking | | Aug 07 17:00 |
| Leonardo Alt, Martin Blicha, Antti Hyvärinen and Natasha Sharygina | SolCMC: Solidity Compiler’s Model Checker | | Aug 07 17:20 |
| Raven Beutner and Bernd Finkbeiner | Software Verification of Hyperproperties Beyond k-Safety | | Aug 08 09:00 |
| Priyanka Golia, Brendan Juba and Kuldeep S. Meel | A Scalable Shannon Entropy Estimator | | Aug 08 09:20 |
| Yuxin Fan, Fu Song, Taolue Chen, Liangfeng Zhang and Wanwei Liu | PoS4MPC: Automated Security Policy Synthesis for Secure Multi-Party Computation | | Aug 08 09:40 |
| Norine Coenen, Raimund Dachselt, Bernd Finkbeiner, Hadar Frenkel, Christopher Hahn, Tom Horak, Niklas Metzger and Julian Siber | Explaining Hyperproperty Violations | | Aug 08 10:00 |
| Elvira Albert, Marta Bellés-Muñoz, Miguel Isabel, Clara Rodríguez-Núñez and Albert Rubio | Distilling Constraints in Zero-Knowledge Protocols | | Aug 08 10:20 |
| Ryotaro Banno, Kotaro Matsuoka, Naoki Matsumoto, Song Bian, Masaki Waga and Kohei Suenaga | Oblivious Online Monitoring for Safety LTL Specification via Fully Homomorphic Encryption | | Aug 08 14:00 |
| Anna Becchi and Alessandro Cimatti | Abstraction Modulo Stability for Reverse Engineering | | Aug 08 14:20 |
| Stanley Bak, Sergiy Bogomolov, Brandon Hencey, Niklas Kochdumper, Ethan Lew and Kostiantyn Potomkin | Reachability of Koopman Linearized Systems Using Random Fourier Feature Observables and Polynomial Zonotope Refinement | | Aug 08 14:40 |
| Eric Goubault and Sylvie Putot | RINO: Robust INner and Outer Approximated Reachability of Neural Networks Controlled Systems | | Aug 08 15:00 |
| Geunyeol Yu, Jia Lee and Kyungmin Bae | STLmc: Robust STL Model Checking of Hybrid Systems using SMT | | Aug 08 15:10 |
| Elizabeth Polgreen, Kevin Cheang, Pranav Gaddamadugu, Adwait Godbole, Kevin Laeufer, Shaokai Lin, Yatin A. Manerkar, Federico Mora and Sanjit A. Seshia | UCLID5: Multi-Modal Formal Modeling, Verification, and Synthesis | | Aug 08 15:20 |
| Chaitanya Agarwal, Shibashis Guha, Jan Křetínský and Pazhamalai Muruganandham | PAC Statistical Model Checking of Mean Payoff in Discrete- and Continuous-Time MDP | | Aug 08 16:00 |
| Thom Badings, Nils Jansen, Sebastian Junges, Marielle Stoelinga and Matthias Volk | Sampling-Based Verification of CTMCs with Uncertain Rates | | Aug 08 16:20 |
| Pablo Castro, Pedro R. D'Argenio, Luciano Putruele and Ramiro Demasi | Playing Against Fair Adversaries in Stochastic Games with Total Rewards | | Aug 08 16:40 |
| Lorenz Leutgeb, Georg Moser and Florian Zuleger | Automated Expected Amortised Cost Analysis of Probabilistic Data Structures | | Aug 08 17:00 |
| Aina Niemetz, Mathias Preiner and Clark Barrett | Murxla: A Modular and Highly Extensible API Fuzzer for SMT Solvers | | Aug 08 17:20 |
| Kyveli Doveri, Pierre Ganty and Nicolas Mazzocchi | FORQ-based Language Inclusion Formal Testing | | Aug 09 11:00 |
| Thibault Dardinier, Gaurav Parthasarathy, Noé Weeks, Peter Müller and Alexander J. Summers | Sound Automation of Magic Wands | | Aug 09 11:20 |
| Yong Li, Andrea Turrini, Weizhi Feng, Moshe Vardi and Lijun Zhang | Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition | | Aug 09 11:40 |
| Alexandre Duret-Lutz, Etienne Renault, Maximilien Colange, Florian Renkin, Alexandre Gbaguidi Aisse, Philipp Schlehuber-Caissier, Thomas Medioni, Antoine Martin, Jérôme Dubois, Clément Gillard and Henrich Lauko | From Spot 2.0 to Spot 2.10: What's New? | | Aug 09 12:00 |
| Vojtěch Havlena, Ondrej Lengal and Barbora Šmahlíková | Complementing Büchi Automata with Ranker | | Aug 09 12:10 |
| Andres Noetzli, Andrew Reynolds, Haniel Barbosa, Clark Barrett and Cesare Tinelli | Even Faster Conflicts and Lazier Reductions for String Solvers | | Aug 09 14:00 |
| Shaowei Cai, Bohan Li and Xindi Zhang | Local Search For SMT on Linear Integer Arithmetic | | Aug 09 14:20 |
| Marco Faella and Gennaro Parlato | Reasoning about Data Trees using CHCs | | Aug 09 14:40 |
| Joshua M. Cohen, Qinshi Wang and Andrew W. Appel | Verified Erasure Correction in Coq with MathComp and VST | | Aug 09 15:00 |
| Shenghao Yuan, Frédéric Besson, Jean-Pierre Talpin, Samuel Hym, Koen Zandberg and Emmanuel Baccelli | End-to-end Mechanised Proof of an eBPF Virtual Machine for Microcontrollers | | Aug 09 15:20 |
| Joonwon Choi, Adam Chlipala and Arvind | Hemiola: A DSL and Verification Tools to Guide Design and Proof of Hierarchical Cache-Coherence Protocols | | Aug 09 15:40 |
| Kishor Jothimurugan, Suguman Bansal, Osbert Bastani and Rajeev Alur | Specification-Guided Learning of Nash Equilibria with High Social Welfare | | Aug 10 14:00 |
| Jingbo Wang, Yannan Li and Chao Wang | Synthesizing Fair Decision Trees via Iterative Constraint Solving | | Aug 10 14:20 |
| Seongwon Bang, Seunghyeon Nam, Inwhan Chun, Ho Young Jhoo and Juneyoung Lee | SMT-based Translation Validation for Machine Learning Compiler | | Aug 10 14:40 |
| Ji Guan, Wang Fang and Mingsheng Ying | Verifying Fairness in Quantum Machine Learning | | Aug 10 15:00 |
| Timo P. Gros, Holger Hermanns, Joerg Hoffmann, Michaela Klauck, Maximilian Alexander Köhl and Verena Wolf | MoGym: Using Formal Models for Training and Verifying Decision-making Agents | | Aug 10 15:20 |
| Mateus De Oliveira Oliveira | Synthesis and Analysis of Petri Nets from Causal Specifications | | Aug 10 16:00 |
| Michael Blondin, Filip Mazowiecki and Philip Offtermatt | Verifying generalised and structural soundness of workflow nets via relaxations | | Aug 10 16:20 |
| Andreas Katis, Anastasia Mavridou, Dimitra Giannakopoulou, Thomas Pressburger and Johann Schumann | Capture, Analyze, Diagnose: Realizability Checking of Requirements in FRET | | Aug 10 16:40 |
| Bernd Finkbeiner, Niklas Metzger and Yoram Moses | Information Flow Guided Synthesis | | Aug 10 16:50 |
| Andreas Gittis, Eric Vin and Daniel Fremont | Randomized Synthesis for Diversity and Cost Constraints with Control Improvisation | | Aug 10 17:10 |
