Buch, Englisch, 634 Seiten, Format (B × H): 155 mm x 235 mm
24th International Conference, SEFM 2026, Valetta, Malta, November 23–27, 2026, Proceedings
Buch, Englisch, 634 Seiten, Format (B × H): 155 mm x 235 mm
Reihe: Lecture Notes in Computer Science
ISBN: 978-3-032-45780-6
Verlag: Springer
This volume constitutes the papers presented at the 24th International Conference on Software Engineering and Formal Methods, SEFM 2026, held in Valetta, Malta, during November 23 - 27, 2026.
The 33 full papers, 1 short paper and 2 tool papers included in these proceedings were carefully reviewed and selected from 80 submissions. They were organized in the following topical sections: Formal Verification and Program Reasoning ; Testing, Monitoring and Assurance; Security, Safety and Dependable Systems; AI and Machine Learning Verification.
Zielgruppe
Research
Autoren/Hrsg.
Fachgebiete
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Algorithmen & Datenstrukturen
- Interdisziplinäres Wissenschaften Wissenschaften: Forschung und Information Informationstheorie, Kodierungstheorie
- Mathematik | Informatik EDV | Informatik Informatik Künstliche Intelligenz
- Mathematik | Informatik EDV | Informatik Programmierung | Softwareentwicklung Software Engineering
- Mathematik | Informatik EDV | Informatik Technische Informatik
Weitere Infos & Material
.- Formal Verification and Program Reasoning .
.- Practical Range Refinement Types with Inference..
.- Modular Composition of Inductive Types Using Lean Meta-programming.
.- Efficient Verification of C Programs with Pointers, Structs, and Arrays..
.- Borderlines of Soundness: Verifying C Aliasing Properties.
.- PETRIFY: Petri-net Based Analysis of Concurrency Properties in Java Bytecode.
.- Automata-Guided Local Proof Obligations for Temporal Safety in Synchronous Programs.
.- Verifying Numerical Methods with Isabelle/HOL .
.- Encodability Criteria for Labelled Semantics.
.- Verifying a Rust Bitmap Allocator in RocQ.
.- KeY4CATs: A Deductive Verification Tool for Context-aware Trace Contracts.
.- Testing, Monitoring and Assurance.
.- Integrating Parallel Trace Abstraction and Explicit Exploration for Test-Case Generation.
.- Metamorphic Testing for Floating-Point Performance Issues in SMT Solvers.
.- Diverse Counterexample Pools for Hybrid Automata: Generation and Selection.
.- Revisiting Sequentialization of Concurrent C Programs.
.- Formal Verification of Stability in Provisioning Changes with BPlan.
.- Runtime Verification of Communicating Systems Using Data-Aware Interaction Models and Broker-Based Observations.
.- Verifying Autoware Controller Node by Combining Model Verification and Runtime Monitoring.
.- Policy-Guided Test Generation for Autonomous Driving Systems via Probabilistic Model Checking.
.- Why3-py: A Tool for Formal Verification of Hypothesis Testing and Meta Analysis in Python.
.- Security, Safety and Dependable Systems.
.- Robust Skill Execution for Autonomous Robots.
.- Protecting Sensitive Data Against Deductions in Business Processes: Formal Semantics and Model-Checking.
.- A Formal Case Study of Side-Channel Attacks on a Water Supply System.
.- Formally Verifying Noir Zero Knowledge Programs with NAVe.
.- SMAC: A Calculus for Verifying Memory Arrays in Isabelle/Solidity.
.- Formal Verification of a Blockchain-Based Healthcare Consent Management Protocol.
.- Verification of a Configurable Railway Protection System: Pushing the Envelope.
.- Automated Abstraction Refinement for Information Flow Security in Embedded Systems.
.- Formal Verification of Credential Provisioning in ISO 15118 Park-and-Charge and Introducing Secure Ownership Transfer.
.- AI and Machine Learning Verification.
.- Discovering Markovian Models from Event Logs for Resource-Aware Process Analysis.
.- Another Brick in the Loop: From Graphical Loop Invariant to Formal Proofs.
.- Don't Blame the Model, Verify the Data: An Evaluation of SMT-based Dataset Verification.
.- Navigating the Random Forest: Verifying ML Models in Safety-Critical Applications with SMT Solvers.
.- Bridging the Integration Bottleneck: A Java Architecture for Model Checking Guided Reinforcement Learning.
.- Reactive Correspondence Relationships for Incremental Triple Graph Grammar Style Model Synchronisation.
.- The Scaffolding Paradox: Evidence from AI-Assisted Dafny Proof Synthesis.
.- Functional Basis Reduction of Neural Networks via Approximate Hidden-Neuron Lumping.
