E-raamat: Formal Methods and Software Engineering: 26th International Conference on Formal Engineering Methods, ICFEM 2025, Hangzhou, China, November 10-13, 2025, Proceedings

.- 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.