Verification, Model Checking, and Abstract Interpretation 25th International Conference, VMCAI 2024, London, United Kingdom, January 15–16, 2024, Proceedings, Part I

Part I: Abstract interpretation; infinite-state systems; model checking and synthesis; SAT, SMT, and automated reasoning; 

Part II: Concurrency; neural networks; probabilistic and quantum programs; program and system verification; runtime verification; security and privacy.

Abstract Interpretation.- Formal Runtime Error Detection During Development in the Automotive Industry.- Abstract Interpretation-Based Feature Importance for Support Vector Machines.- Generation of Violation Witnesses by Under-Approximating Abstract Interpretation.- Correctness Witness Validation by Abstract Interpretation.- Infinite-State Systems.- Project and Conquer: Fast Quantifier Elimination for Checking Petri Net Reachability.- Parameterized Verification of Disjunctive Timed Networks.- Resilience and Home-Space for WSTS.- Model Checking and Synthesis.- Generic Model Checking for Modal Fixpoint Logics in COOL-MC.- Model-Guided Synthesis for LTL over Finite Traces.- Solving Two-Player Games under Progress Assumptions.- AT, SMT, and Automated Reasoning Interpolation and Quantifiers in Ortholattices.- Function Synthesis for Maximizing Model Counting.- Boosting Constrained Horn Solving by Unsat Core Learning.- On the Verification of a Subgraph Construction Algorithm.- Efficient Local Search for Nonlinear Real Arithmetic.