This book constitutes the refereed proceedings of the 25th International Symposium on Formal Methods, FM 2023, which took place in Lübeck, Germany, in March 2023. The 26 full paper, 2 short papers included in this book were carefully reviewed and selected rom 95 submissions. They have been organized in topical sections as follows: SAT/SMT; Verification; Quantitative Verification; Concurrency and Memory Models; Formal Methods in AI; Safety and Reliability. The proceedings also contain 3 keynote talks and 7 papers from the industry day.
Reihe
Auflage
Sprache
Verlagsort
Verlagsgruppe
Springer International Publishing
Illustrationen
1098
132 farbige Abbildungen, 1098 s/w Abbildungen
XVI, 659 p. 1230 illus., 132 illus. in color.
ISBN-13
978-3-031-27481-7 (9783031274817)
DOI
10.1007/978-3-031-27481-7
Schweitzer Klassifikation
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.
