RESEARCH PAPERS
- Split Gröbner Bases for Satisfiability Modulo Finite Fields
Alex Ozdemir, Shankara Pailoor, Alp Bassa, Kostas Ferles, Clark Barrett and Işil Dillig - SMT-based Symbolic Model-Checking for Operator Precedence Languages
Michele Chiari, Luca Geatti, Nicola Gigante and Matteo Pradella - Proactive Real-Time First-Order Enforcement
François Hublet, Leonardo Lima, David Basin, Srdjan Krstic and Dmitriy Traytel - Information Flow guided Synthesis with Unbounded Communication
Bernd Finkbeiner, Niklas Metzger and Yoram Moses - Relational Synthesis of Recursive Programs via Constraint Annotated Tree Automaton
Anders Miltner, Ziteng Wang, Swarat Chaudhuri and Isil Dillig - Simulating Quantum Circuits by Model Counting
Jingyi Mei, Marcello Bonsangue and Alfons Laarman - Efficient Implementation of an Abstract Domain of Quantified First-Order Formulas
Eden Frenkel, Tej Chajed, Oded Padon and Sharon Shoham - Boosting Few-Pixel Robustness Verification via Covering Verification Designs
Yuval Shapira, Naor Wiesel, Shahar Shabelman and Dana Drachsler-Cohen - Verifying Global Two-Safety Properties in Neural Networks with Confidence
Anagha Athavale, Ezio Bartocci, Maria Christakis, Matteo Maffei, Dejan Nickovic and Georg Weissenbacher - Toward Liveness Proofs at Scale
Kenneth McMillan - End-to-end Mechanized Proof of a JIT-accelerated eBPF Virtual Machine for IoT
Shenghao Yuan, Frédéric Besson and Jean-Pierre Talpin - Synthesis of Temporal Causality
Bernd Finkbeiner, Hadar Frenkel, Niklas Metzger and Julian Siber - Dynamic Programming for Symbolic Boolean Realizability and Synthesis
Yi Lin, Moshe Vardi and Lucas Martinelli Tabajara - Measurement-based Verification of Quantum Markov Chains
Ji Guan, Yuan Feng, Andrea Turrini and Mingsheng Ying - Verification Algorithms for Automated Separation Logic Verifiers
Marco Eilers, Malte Schwerhoff and Peter Müller - Lexicographic Ranking Supermartingales with Lazy Lower Bounds
Toru Takisaka, Libo Zhang, Changjiang Wang and Jiamou Liu - Quantified Linear Arithmetic Satisfiability Via Fine-grained Strategy Improvement
Charlie Murphy and Zachary Kincaid - Strided Difference Bound Matrices
Arjun Pitchanathan, Albert Cohen, Oleksandr Zinenko and Tobias Grosser - General Anticipatory Runtime Verification
Raik Hipler, Hannes Kallwies, Martin Leucker and César Sánchez - Certified Robust Accuracy of Neural Networks Are Bounded due to Bayes Errors
Ruihan Zhang and Jun Sun - Using Four-Valued Signal Temporal Logic for Incremental Verification of Hybrid Systems
Florian Lercher and Matthias Althoff - Localized Attractor Computations for Infinite-State Games
Philippe Heim, Satya Prakash Nayak, Rayna Dimitrova and Anne-Kathrin Schmuck - The Top-Down Solver Verified: Building Confidence in Static Analyzers
Yannick Stade, Sarah Tilscher and Helmut Seidl - Bisimulation Learning
Alessandro Abate, Mirco Giacobbe and Yannik Schnitzer - Regular Reinforcement Learning
Taylor Dohmen, Mateo Perez, Fabio Somenzi and Ashutosh Trivedi - Collective Contracts for Message-Passing Parallel Programs
Ziqing Luo and Stephen F. Siegel - Distributed SMT Solving Based on Dynamic Variable-level Partitioning
Mengyu Zhao, Shaowei Cai and Yuhang Qian - LTL learning on GPUs
Mojtaba Valizadeh, Nathanael Fijalkow and Martin Berger - Algebraic Reasoning Meets Automata in Solving Linear Integer Arithmetic
Peter Habermehl, Vojtěch Havlena, Michal Hečko, Lukáš Holík and Ondrej Lengal - Compositional Value Iteration with Pareto Caching
Kazuki Watanabe, Marck van der Vegt, Sebastian Junges and Ichiro Hasuo - Formally Certified Approximate Model Counting
Yong Kiam Tan, Jiong Yang, Mate Soos, Magnus O. Myreen and Kuldeep S. Meel - Breaking the Mold: Nonlinear Ranking Function Synthesis without Templates
Shaowei Zhu and Zachary Kincaid - What should be observed for optimal reward in POMDPs?
Alyzia-Maria Konsta, Alberto Lluch Lafuente and Christoph Matheja - Verifying Cake Cutting, Faster
Noah Bertram, Tean Lai and Justin Hsu - Probabilistic Access Policies with Automated Reasoning Support
Shaowei Zhu and Yunbo Zhang - Syntax-Guided Automated Program Repair For Hyperproperties
Raven Beutner, Tzu-Han Hsu, Borzoo Bonakdarpour and Bernd Finkbeiner - Avoiding the Shoals – A New Approach to Liveness Checking
Yechuan Xia, Alessandro Cimatti, Alberto Griggio and Jianwen Li - Approximate Relational Reasoning for Quantum Programs
Peng Yan, Hanru Jiang and Nengkun Yu - From Clauses to Klauses
Joseph Reeves, Marijn Heule and Randal Bryant - Predictive Monitoring with Strong Trace Prefixes
Zhendong Ang and Umang Mathur - Unifying Qualitative and Quantitative Safety Verification of DNN-Controlled Systems
Dapeng Zhi, Peixin Wang, Si Liu, Luke Ong and Min Zhang - On Polynomial Expressions with C-Finite Recurrences in Loops with Nested Nondeterministic Branches
Chenglin Wang and Fangzhen Lin - Parsimonious Optimal Dynamic Partial Order Reduction
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson and Konstantinos Sagonas - Optimization-Based Model Checking for Complex STL Specifications
Sota Sato, Jie An, Zhenya Zhang and Ichiro Hasuo - Guiding Enumerative Program Synthesis with Large Language Models
Yixuan Li, Julian Parsert and Elizabeth Polgreen - Scenario-based Flexible Modeling and Scalable Falsification for Reconfigurable CPSs
Jiawan Wang, Wenxia Liu, Muzimiao Zhang, Jiaqi Wei, Yuhui Shi, Lei Bu and Xuandong Li - Scalable Bit-Blasting with Abstractions
Aina Niemetz, Mathias Preiner and Yoni Zohar - Safe Exploration in Reinforcement Learning by Reachability Analysis over Learned Models
Yuning Wang and He Zhu - Stochastic Omega-Regular Verification and Control with Supermartingales
Alessandro Abate, Mirco Giacobbe and Diptarko Roy - Inner-approximate Reachability Computation via Zonotopic Boundary Analysis
Dejin Ren, Zhen Liang, Chenyu Wu, Jianqiang Ding, Taoran Wu and Bai Xue - Enchanting Program Specification Synthesis by Large Language Models using Static Analysis and Program Verification
Cheng Wen, Jialun Cao, Jie Su, Zhiwu Xu, Shengchao Qin, Mengda He, Haokun Li, Shing-Chi Cheung and Cong Tian
TOOL PAPERS
- A Framework for Debugging Automated Program Verification Proofs via Proof Actions
Chanhee Cho, Yi Zhou, Jay Bosamiya and Bryan Parno - The VerCors Verifier: a Progress Report
Lukas Armborst, Pieter Bos, Lars van den Haak, Marieke Huisman, Robert Rubbens, Ömer Sakar and Philip Tasche - Symbolic Model-Checking Intermediate-Language Tool Suite
Chris Johannsen, Karthik Nukala, Rohit Dureja, Ahmed Irfan, Natarajan Shankar, Cesare Tinelli, Moshe Y. Vardi and Kristin Yvonne Rozier - Playing Games with your PET: Extending the Partial Exploration Tool to Stochastic Games
Tobias Meggendorfer and Maximilian Weininger - CaDiCaL 2.0
Armin Biere, Tobias Faller, Katalin Fazekas, Mathias Fleury, Nils Froleyks and Florian Pollitt - Interactive Theorem Proving modulo Fuzzing
Sujit Muduli, Rohan Padulkar and Subhajit Roy - soid: A Tool for Legal Accountability for Automated Decision Making
Samuel Judson, Matthew Elacqua, Filip Cano, Timos Antonopoulos, Bettina Könighofer, Scott Shapiro and Ruzica Piskac - SMLP: Symbolic Machine Learning Prover
Franz Brauße, Zurab Khasidashvili and Konstantin Korovin - Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
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 - The SemGuS Toolkit
Keith J.C. Johnson, Andrew Reynolds, Thomas Reps and Loris D’Antoni - hevm, a Fast Symbolic Execution Framework for EVM Bytecode
Dxo, Mate Soos, Zoe Paraskevopoulou, Martin Lundfall and Mikael Brockman - Monitizer: Automating Design and Evaluation of Neural Network Monitors
Muqsit Azeem, Marta Grobelna, Sudeep Kanav, Jan Kretinsky, Stefanie Mohr and Sabine Rieder - Arithmetic Solving in Z3
Nikolaj Bjørner and Lev Nachmanson - SolTG: A CHC-based Solidity Test Case Generator
Konstantin Britikov, Ilia Zlatkin, Grigory Fedyukovich, Leonardo Alt and Natasha Sharygina - QReach: A Reachability Analysis Tool for Quantum Markov Chains
Aochu Dai and Mingsheng Ying - mypyvy: A Research Platform for Verification of Transition Systems in First-Order Logic
James R. Wilcox, Yotam M. Y. Feldman, Oded Padon and Sharon Shoham
INDUSTRIAL EXPERIENCE REPORTS OR CASE STUDIES
- Testing the migration from analogical to software-based Railway Interlocking Systems
Anna Becchi, Alessandro Cimatti and Giuseppe Scaglione - Monitoring Unmanned Aircraft: Specification, Integration, and Lessons-learned
Jan Baumeister, Bernd Finkbeiner, Florian Kohn, Sebastian Schirmer, Christoph Torens, Florian Löhr and Guido Manfredi
PROCEEDING ACCESS
Conference participants have free access to the conference proceedings starting on 24th July 2024 for 4 weeks. Please use the following links: