Invited Talk.-A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems
Model Checking
Bounded Model Checking for Asynchronous Hyperproperties
Model Checking Linear Dynamical Systems under Floating-point Rounding
Efficient Loop Conditions for Bounded Model Checking Hyperproperties
Reconciling Preemption Bounding with DPOR
Optimal Stateless Model Checking for Causal Consistency
Symbolic Model Checking for TLA+ Made Faster
AutoHyper: Explicit-State Model Checking for HyperLTL
Machine Learning/Neural Networks
Feature Necessity & Relevancy in ML Classifier Explanations
Towards Formal XAI: Formally Approximate Minimal Explanations of Neural Networks
OccRob: Effcient SMT-Based Occlusion Robustness Verification of Deep Neural Networks
Neural Network-Guided Synthesis of Recursive List Functions
Automata
Modular Mix-and-Match Complementation of Buechi automata
Validating Streaming JSON Documents With Learned VPAs
Antichains Algorithms for the Inclusion Problem Between -VPL
Stack-Aware Hyperproperties
Proofs
Propositional Proof Skeletons
Unsatisfiability Proofs for Distributed Clause-Sharing SAT Solvers
Carcara: An effcient proof checker and elaborator for SMT proofs in the Alethe format
Constraint Solving/Blockchain
The Packing Chromatic Number of the Infinite Square Grid is 15
Active Learning for SAT Solver Benchmarking
ParaQooba: A Fast and Flexible Framework for Parallel and Distributed QBF Solving
Inferring Needless Write Memory Accesses on Ethereum Bytecode
Markov Chains/Stochastic Control
A Practitioner's Guide to MDP Model Checking Algorithms
Correct Approximation of Stationary Distributions
Robust Almost-Sure Reachability in Multi-Environment MDPs
Mungojerrie: Linear-Time Objectives in Model-Free Reinforcement Learning
Verification
A Formal CHERI-C Semantics for Verification
Automated Verification for Real-Time Systems via Implicit Clocks and an Extended Antimirov Algorithm
Parameterized Verification under TSO with Data Types
Verifying Learning-Based Robotic Navigation Systems: A Case Study
Make flows small again: revisiting the flow framework
ALASCA: Reasoning in Quantified Linear Arithmetic
A Matrix-Based Approach to Parity Games
A GPU Tree Database for Many-Core Explicit State Space Exploration.