LEADER 05938nam 22007695 450 001 9910678257703321 005 20251113180737.0 010 $a9783031274817 010 $a3031274814 024 7 $a10.1007/978-3-031-27481-7 035 $a(MiAaPQ)EBC7209155 035 $a(Au-PeEL)EBL7209155 035 $a(CKB)26192082600041 035 $a(DE-He213)978-3-031-27481-7 035 $a(PPN)269092676 035 $a(EXLCZ)9926192082600041 100 $a20230302d2023 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aFormal Methods $e25th International Symposium, FM 2023, Lübeck, Germany, March 6?10, 2023, Proceedings /$fedited by Marsha Chechik, Joost-Pieter Katoen, Martin Leucker 205 $a1st ed. 2023. 210 1$aCham :$cSpringer International Publishing :$cImprint: Springer,$d2023. 215 $a1 online resource (661 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v14000 311 08$aPrint version: Chechik, Marsha Formal Methods Cham : Springer International Publishing AG,c2023 9783031274800 320 $aIncludes bibliographical references and index. 327 $aKeynotes -- 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-Aware Autonomous 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. 330 $aThis 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. . 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v14000 606 $aSoftware engineering 606 $aComputer science 606 $aComputers, Special purpose 606 $aProgramming languages (Electronic computers) 606 $aMicroprogramming 606 $aNatural language processing (Computer science) 606 $aSoftware Engineering 606 $aComputer Science Logic and Foundations of Programming 606 $aSpecial Purpose and Application-Based Systems 606 $aProgramming Language 606 $aControl Structures and Microprogramming 606 $aNatural Language Processing (NLP) 615 0$aSoftware engineering. 615 0$aComputer science. 615 0$aComputers, Special purpose. 615 0$aProgramming languages (Electronic computers) 615 0$aMicroprogramming. 615 0$aNatural language processing (Computer science) 615 14$aSoftware Engineering. 615 24$aComputer Science Logic and Foundations of Programming. 615 24$aSpecial Purpose and Application-Based Systems. 615 24$aProgramming Language. 615 24$aControl Structures and Microprogramming. 615 24$aNatural Language Processing (NLP). 676 $a004.0151 702 $aKatoen$b Joost-Pieter 702 $aLeucker$b Martin 702 $aChechik$b Marsha 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910678257703321 996 $aFormal methods$92247212 997 $aUNINA