000 05669nam a22006375i 4500
001 978-3-031-27481-7
003 DE-He213
005 20240423125444.0
007 cr nn 008mamaa
008 230302s2023 sz | s |||| 0|eng d
020 _a9783031274817
_9978-3-031-27481-7
024 7 _a10.1007/978-3-031-27481-7
_2doi
050 4 _aQA76.758
072 7 _aUMZ
_2bicssc
072 7 _aCOM051230
_2bisacsh
072 7 _aUMZ
_2thema
082 0 4 _a005.1
_223
245 1 0 _aFormal Methods
_h[electronic resource] :
_b25th International Symposium, FM 2023, Lübeck, Germany, March 6–10, 2023, Proceedings /
_cedited by Marsha Chechik, Joost-Pieter Katoen, Martin Leucker.
250 _a1st ed. 2023.
264 1 _aCham :
_bSpringer International Publishing :
_bImprint: Springer,
_c2023.
300 _aXVI, 659 p. 1230 illus., 132 illus. in color.
_bonline resource.
336 _atext
_btxt
_2rdacontent
337 _acomputer
_bc
_2rdamedia
338 _aonline resource
_bcr
_2rdacarrier
347 _atext file
_bPDF
_2rda
490 1 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v14000
505 0 _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.
520 _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. .
650 0 _aSoftware engineering.
650 0 _aComputer science.
650 0 _aComputers, Special purpose.
650 0 _aProgramming languages (Electronic computers).
650 0 _aMicroprogramming .
650 0 _aNatural language processing (Computer science).
650 1 4 _aSoftware Engineering.
650 2 4 _aComputer Science Logic and Foundations of Programming.
650 2 4 _aSpecial Purpose and Application-Based Systems.
650 2 4 _aProgramming Language.
650 2 4 _aControl Structures and Microprogramming.
650 2 4 _aNatural Language Processing (NLP).
700 1 _aChechik, Marsha.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aKatoen, Joost-Pieter.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
700 1 _aLeucker, Martin.
_eeditor.
_4edt
_4http://id.loc.gov/vocabulary/relators/edt
710 2 _aSpringerLink (Online service)
773 0 _tSpringer Nature eBook
776 0 8 _iPrinted edition:
_z9783031274800
776 0 8 _iPrinted edition:
_z9783031274824
830 0 _aLecture Notes in Computer Science,
_x1611-3349 ;
_v14000
856 4 0 _uhttps://doi.org/10.1007/978-3-031-27481-7
912 _aZDB-2-SCS
912 _aZDB-2-SXCS
912 _aZDB-2-LNC
942 _cSPRINGER
999 _c178131
_d178131