LEADER 04891nam 22007335 450 001 9911047828403321 005 20251111120408.0 010 $a981-9542-13-8 024 7 $a10.1007/978-981-95-4213-0 035 $a(CKB)42609436500041 035 $a(DE-He213)978-981-95-4213-0 035 $a(MiAaPQ)EBC32408455 035 $a(Au-PeEL)EBL32408455 035 $a(EXLCZ)9942609436500041 100 $a20251111d2026 u| 0 101 0 $aeng 135 $aur||||||||||| 181 $ctxt$2rdacontent 182 $cc$2rdamedia 183 $acr$2rdacarrier 200 10$aFormal Methods and Software Engineering $e26th International Conference on Formal Engineering Methods, ICFEM 2025, Hangzhou, China, November 10?13, 2025, Proceedings /$fedited by Étienne André, Jingyi Wang, Naijun Zhan 205 $a1st ed. 2026. 210 1$aSingapore :$cSpringer Nature Singapore :$cImprint: Springer,$d2026. 215 $a1 online resource (XX, 392 p. 108 illus., 76 illus. in color.) 225 1 $aLecture Notes in Computer Science,$x1611-3349 ;$v16229 311 08$a981-9542-12-X 327 $a -- Formal Verification of Physical Layer Security Protocols for Next-Generation Communication Networks. -- Automata-Based Steering of Large Language Models for Diverse Structured Generation. -- LLM-SYM: Integrating Symbolic Methods and Large Language Models for Automated Theorem Proving. -- Modeling and Analysis of Cyber-Physical Systems in the Hybrid pi-Calculus Using Extended Sequence Diagrams. -- Neural-Symbolic System Control Adjustment Based on Runtime Verification. -- Formalizing Requirements into Dafny Specifications with LLMs. -- Detecting Vector Container Errors in C++ Programs via Abstract Interpretation. -- BCCIC3:Batch Clause Construction Enhanced Generalization in IC3. -- MetaLogic: Robustness Evaluation of Text-to-Image Models Using Logically Equivalent Prompts. -- Formal Construction of Threat Detections from Attack Trees. -- A Test-Driven Approach for Refining Use Case Specifications of Software Requirements with LLMs. -- ZK-ProVer: Proving Programming Verification in Non-Interactive Zero-Knowledge Proofs. -- Synthesizing Loops from Linear Ranking Functions. -- Modeling and Verifying Concurrent Reactive Systems Using Separation Logic. -- Formal Modeling and Verification of Blockchain Consensus Protocols: A Case Study on ChainMaker. -- A Unified Method to Efficiently Verify Opacity of Discrete-Timed Automata. -- Quantitative Verification for Temporal Properties of Massive Linear Systems. -- Avoiding Larger Conflict Regions in CDCL-Style Methods for Solving SMT-NRA. -- Formal Modeling of Reinforcement Learning Systems with SMT. -- Formal modelling of fault tolerant robotic missions. -- Towards High-Level SMT Program Modeling: Bounded Integers, Simplified Structs, and Metaprogramming. 330 $aThis volume LNCS 16229 constitutes the refereed proceedings of 26th International Conference on Formal Methods and Software Engineering, ICFEM 2025, in Hangzhou, China, during November 10?13, 2025. The 20 full papers presented were carefully reviewed and selected from 47 submissions. The conference focuses on wide range of research areas, covering both theoretical foundations and practical applications of formal engineering methods. 410 0$aLecture Notes in Computer Science,$x1611-3349 ;$v16229 606 $aComputer science 606 $aComputer programming 606 $aSoftware engineering 606 $aCompilers (Computer programs) 606 $aApplication software 606 $aNatural language processing (Computer science) 606 $aTheory of Computation 606 $aProgramming Techniques 606 $aSoftware Engineering 606 $aCompilers and Interpreters 606 $aComputer and Information Systems Applications 606 $aNatural Language Processing (NLP) 615 0$aComputer science. 615 0$aComputer programming. 615 0$aSoftware engineering. 615 0$aCompilers (Computer programs). 615 0$aApplication software. 615 0$aNatural language processing (Computer science). 615 14$aTheory of Computation. 615 24$aProgramming Techniques. 615 24$aSoftware Engineering. 615 24$aCompilers and Interpreters. 615 24$aComputer and Information Systems Applications. 615 24$aNatural Language Processing (NLP). 676 $a004.0151 702 $aAndré$b Étienne$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aWang$b Jingyi$4edt$4http://id.loc.gov/vocabulary/relators/edt 702 $aZhan$b Naijun$4edt$4http://id.loc.gov/vocabulary/relators/edt 801 0$bMiAaPQ 801 1$bMiAaPQ 801 2$bMiAaPQ 906 $aBOOK 912 $a9911047828403321 996 $aFormal Methods and Software Engineering$9771999 997 $aUNINA