Tools and Algorithms for the Construction and Analysis of Systems

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.