This book constitutes the refereed proceedings of the 20th International Symposium on Theoretical Aspects of Software Engineering, TASE 2026, held in Shanghai, China, during July 4–6, 2026.
The 23 full papers and 5 short papers were carefully selected from 64 submissions. The proceedings aim to bring together researchers and developers from academia and industry with interest in the theoretical aspects of software engineering.
Table of Contents:
.- Automated Trace Link Recovery Between Natural Language Requirements and Formal Specifications via LLMs.
.- The Robustness Profile: A Metamorphic Testing Framework for Multi-Dimensional Evaluation of DRL Agents.
.- Generation of Non-matching Strings for Testing Regular Expressions via Complement Automaton Coverage.
.- Clight2Rust: Translating a Subset of C into Safe Rust with a Small Trusted Runtime.
.- Formal Verification of a Rust-Based Buddy Physical Memory Allocator.
.- Enhancing LLM-based Proof Synthesis for Rust Programs via Semantic Chunking and Hierarchical Context Expansion.
.- Towards Accurate Thread Sharing Analysis via Synchronization-Aware Dynamic Tracing.
.- A HOL Theorem Proving Interface for C.
.- CARET Model Checking of Self Modifying Code.
.- QCP: A Practical Separation Logic-based C Program Verification Tool.
.- Formal Specification-Based Code Review via LLMs.
.- RealSanitizer: Detecting Floating-Point Errors via a Dynamic Precision Oracle.
.- Random Generation of Small Quantitative Automata for Algorithm Debugging.
.- Learning-Based Quantitative Evaluation of GR(1) Temporal Properties upon Partial Data Traces.
.- Learn by Analogy: Distribution-aware Fuzz Testing for DNNs via Cross-Modal Generation.
.- A Formal Quantitative Approach for Evaluating Safety-Critical Driving Scenarios via Statistical Model Checking.
.- Semantics-Based Verification of an Implemented Shor Oracle for ECDLP in Qrisp.
.- Reachable Completeness Theorem of Order-sorted Equational Logic with Infinite Proofs.
.- LLM-Guided Requirement Scenario-Based Testing for Simulink Models.
.- PAT2PRISM: Bridging Qualitative Correctness and Quantitative Resilience for IoT Protocols.
.- From Monolithic to Compositional: A Compositional Operational Semantics for Crystality.
.- Timed Games under Environmental Interference with Real-Time Objectives.
.- Health-State-Aware Adaptive Bad Block Management for NAND Flash–Based Storage Systems.
.- First Steps in a Paraconsistent Transition Systems Toolkit.
.- Scenario matching problem in distributed systems.
.- Intuitive Verification of Sequential Programs Using Hybrid Reasoning.
.- Incremental Reinforcement Learning with Temporally Dependent Goals.
.- Symbolic Model Checking for Linear Temporal Dynamic Logic via Compositional Testers.
