Formal Methods

Keynotes.- Symbolic Computation in Automated Program Reasoning.- The next big thing: from embedded systems to embodied actors.- Intelligent and Dependable Decision-Making Under Uncertainty.- A Coq formalization of Lebesgue Induction Principle and Tonelli's Theorem.- SAT/SMT.- Railway Scheduling Using Boolean Satisfiability Modulo Simulations.- SMT Sampling via Model-Guided Approximation.- Efficient SMT-based Network Fault Tolerance Verification.- Verification I.- Formalising the Prevention of Microarchitectural Timing Channels by Operating Systems.- Can we Communicate? Using Dynamic Logic to Verify Team Automata.- The ScalaFix equation solver.- HHLPy: Practical Verification of Hybrid Systems using Hoare Logic.- Quantitative Verification.- symQV: Automated Symbolic Verification of Quantum Programs.- PFL: a Probabilistic Logic for Fault Trees.- Energy BuechiProblems.- QMaude: quantitative specification and verification in rewriting logic.- Concurrency and Memory Models.- Minimisation of Spatial Models using Branching Bisimilarity.- Reasoning about Promises in Weak Memory Models with Event Structures.- A fine-grained semantics for arrays and pointers under weak memory models.- VeyMont: Parallelising Verified Programs instead of Verifying Parallel Programs.- Verification 2.- Verifying At the Level of Java Bytecode.- Abstract Alloy Instances.- Monitoring the Internet Computer.- Word Equations in Synergy with Regular Constraints.- Formal Methods in AI.- Verifying Feedforward Neural Networks for Classification in Isabelle/HOL.- SMPT: A Testbed for Reachabilty Methods in Generalized Petri Nets.- The Octatope Abstract Domain for Verification of Neural Networks.- Program Semantics and Verification Technique for AI-centred Programs.- Safety and Reliability.- Tableaux for Realizability of Safety Specifications.- A Decision Diagram Operation for Reachability.- Formal Modelling of Safety Architecture for Responsibility-AwareAutonomous Vehicle via Event-B Refinement.- A Runtime Environment for Contract Automata.- Industry Day.- Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny.- Shifting Left for Early Detection of Machine-Learning Bugs.- A Systematic Approach to Automotive Security.- Specification-Guided Critical Scenario Identification for Automated Driving.- Runtime Monitoring for Out-of-Distribution Detection in Object Detection Neural Networks.- Backdoor Mitigation in Deep Neural Networks via Strategic Retraining.- veriFIRE: Verifying an Industrial, Learning-Based Wildfire Detection System.