LEADER 04576nam 22007455 450 001 9910799214203321 005 20240627180810.0 010 $a3-031-50521-2 024 7 $a10.1007/978-3-031-50521-8 035 $a(MiAaPQ)EBC31051282 035 $a(Au-PeEL)EBL31051282 035 $a(CKB)29510229700041 035 $a(DE-He213)978-3-031-50521-8 035 $a(EXLCZ)9929510229700041 100 $a20231229d2024 u| 0 101 0 $aeng 135 $aurcnu|||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aVerification, Model Checking, and Abstract Interpretation $e25th International Conference, VMCAI 2024, London, United Kingdom, January 15?16, 2024, Proceedings, Part II /$fedited by Rayna Dimitrova, Ori Lahav, Sebastian Wolff 205 $a1st ed. 2024. 210 1$aCham :$cSpringer Nature Switzerland :$cImprint: Springer,$d2024. 215 $a1 online resource (349 pages) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v14500 311 08$aPrint version: Dimitrova, Rayna Verification, Model Checking, and Abstract Interpretation Cham : Springer International Publishing AG,c2024 9783031505201 320 $aIncludes bibliographical references and index. 327 $aConcurrency -- Petrification: Software Model Checking for Programs with Dynamic Thread Management -- A Fully Verified Persistency Library -- A Navigation Logic for Recursive Programs with Dynamic Thread Creation -- Neural Networks -- Taming Reachability Analysis of DNN-Controlled Systems via Abstraction-Based Training -- Verification of Neural Networks' Local Differential Classification Privacy -- AGNES: Abstraction-guided Framework for Deep Neural Network Security -- Probabilistic and Quantum Programs Guaranteed inference for probabilistic programs: a parallelisable, small-step operational approach -- Local Reasoning about Probabilistic Behaviour for Classical-Quantum Programs -- Program and System Verification -- Deductive Verification of Parameterized Embedded Systems modeled in SystemC -- Automatically Enforcing Rust Trait Properties -- Borrowable Fractional Ownership Types for Verification -- Runtime Verification -- TP-DejaVu: Combining Operational and Declarative Runtime Verification -- Synthesizing Efficiently Monitorable Formulas in Metric Temporal Logic -- Security and Privacy -- Automatic and Incremental Repair for Speculative Information Leaks -- Sound Abstract Nonexploitability Analysis. 330 $aThe two-volume set LNCS 14499 and 14500 constitutes the proceedings of the 25th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2024, which took place in London, Ontario, Canada, in January 2024. The 30 full papers presented in the proceedings were carefully reviewed and selected from 74 submissions. They were organized in topical sections as follows: 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; . 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v14500 606 $aComputer science 606 $aComputer science$xMathematics 606 $aLogic programming 606 $aComputers, Special purpose 606 $aSoftware engineering 606 $aMicroprogramming 606 $aTheory of Computation 606 $aMathematics of Computing 606 $aLogic in AI 606 $aSpecial Purpose and Application-Based Systems 606 $aSoftware Engineering 606 $aControl Structures and Microprogramming 615 0$aComputer science. 615 0$aComputer science$xMathematics. 615 0$aLogic programming. 615 0$aComputers, Special purpose. 615 0$aSoftware engineering. 615 0$aMicroprogramming. 615 14$aTheory of Computation. 615 24$aMathematics of Computing. 615 24$aLogic in AI. 615 24$aSpecial Purpose and Application-Based Systems. 615 24$aSoftware Engineering. 615 24$aControl Structures and Microprogramming. 676 $a005.14 702 $aDimitrova$b Rayna 702 $aLahav$b Ori 702 $aWolff$b Sebastian 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9910799214203321 996 $aVerification, Model Checking, and Abstract Interpretation$92593983 997 $aUNINA