From Mechanized Semantics to Verified Compilation: The Clight Semantics of CompCert.- Foundations for Query-based Runtime Monitoring of Temporal Properties over Runtime Models.- Probabilistic Runtime Enforcement of Executable BPMN Processes.- Integrating Look-ahead Design-time and Run-time Control-synthesis for Graph Transformation Systems.- Formal Specification of Trusted Execution Environment APIs.- Monitoring the Future of Smart Contracts.- Comprehending Object State via Dynamic Class Invariant Learning.- Detection for Large-Scale Online Service Systems Using Multi-Channel Data.

- Refinement Verification of OS Services based on a Verified Preemptive Microkernel.- Fuzzy quantitative attack tree analysis.- Towards Reliable SQL Synthesis: Fuzzing-Based Evaluation and Disambiguation.- Invariant-based Program Repair.- Can ChatGPT support software verification.- Combining Deductive Verification with Shape Analysis.- First Steps towards Deductive Verification of LLVM IR.- FDSE: Enhance Symbolic Execution by Fuzzing-based Pre-Analysis (Competition Contribution).

- Fizzer: New Gray-Box Fuzzer (Competition Contribution).- KLEEF: Symbolic Execution Engine (Competition Contribution).- TracerX: Pruning Dynamic Symbolic Execution with Deletion and Weakest Precondition Interpolation (Competition Contribution).- Ultimate TestGen: Test Case Generation with Automata-based Software Model Checking (Competition Contribution).