ASYDE 2026 – Preliminary Table of Contents

8th International Workshop on Automated and verifiable Software sYstem DEvelopment (ASYDE 2026)

Frontmatter

Papers

Constrained Automated Requirements Formalization for Rigorous Analysis with Alloy
Viktoria Koscinski and Mehdi Tarrit Mirakhorli
(Colorado State University, USA; University of Hawaii at Manoa, USA)
Early detection of security flaws in software requirements is crucial yet challenging due to the inherent ambiguity of natural language (NL) specifications. While manual reviews are labor-intensive and lack formal rigor, automated formal verification remains bottlenecked by the steep expertise barrier required for manual specification. This paper addresses these challenges through Constrained Automated Requirements Formalization (CARF). Instead of generating arbitrary formal formulas from scratch, our approach restricts the translation domain by leveraging Large Language Models (LLMs) to map unstructured NL requirements onto a predefined, bounded logic of an existing framework for common design weaknesses. We evaluate our methodology across five real-world security requirements datasets against traditional heuristic baselines. The experimental results demonstrate that CARF is robust, successfully outperforming keyword matching and showing structural resilience to minor translation imperfections when identifying missing design controls. We position our tool as a powerful collaborative assistant that significantly lowers the barrier to adopting formal security verification methods during the early software design lifecycle.
Publisher's Version Article: asews26asydemain-id4-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844526

Controller Mimicking for On-the-Fly DES Reachability Control
Florencia Zanollo, Fuyuki Ishikawa, Sebastian Uchitel, and Víctor A. Braberman
(University of Buenos Aires, Argentina; CONICET, Argentina; National Institute of Informatics, Japan; Imperial College London, UK; Universidad de San Andres, Argentina)
One of the primary challenges in synthesizing controllers for Discrete Event Systems (DES) is the exponential growth of the composed state space. On-the-fly Directed Controller Synthesis (OTF-DCS) mitigates this by incrementally exploring the system, but its performance depends on the quality of the exploration heuristic. Recent reinforcement learning approaches learn effective heuristics but require repeatedly executing the expensive OTF-DCS algorithm during training, making the process computationally heavy.
In this work, we propose CMRL, a Controller Mimicking Reinforcement Learning approach that trains a Deep Q-Network agent directly as a reachability controller on a pre-labeled monolithic plant. By using a fast simulation environment derived from a solution, CMRL completely decouples training from the costly on-the-fly synthesis procedure. This yields substantially lower training times (up to 81% reduction) while still delivering synthesis-time effectiveness that is on par with previous approaches.
Publisher's Version Article: asews26asydemain-id6-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844527

Correct-by-Construction Evolution of Digital Twins for Real-Time Autonomous Systems
Luca Brodo, Giuseppe Scalora, and Stefan Henkler
(Hamm-Lippstadt University of Applied Sciences, Germany)
Safety-critical cyber-physical systems must evolve---through adaptation and post-deployment updates---without forfeiting the guarantees on which their certification rests. Yet digital-twin (DT)--based model-based systems engineering (MBSE) lacks a formal mechanism for preserving correctness as the physical twin (PT) and its DT co-evolve. We argue that refinement can play this role twice: as a correctness guarantee and as a constructive device that automates deployment. We present a refinement-based paradigm for DT-based MBSE that organizes correctness into a small set of locally verifiable obligations over a multi-view decomposition and two flows for design and evolution. The central evolution obligation is instantiated by Relaxed Weak Timed Bisimulation (RWTBS), which allows a DT to propose updates to its PT that preserve output-timing while tolerating bounded input-timing flexibility. The same discipline then compiles timed automata into FreeRTOS and ROS~2 code that refines its model up to a single bounded relaxation---correct by construction.
Publisher's Version Article: asews26asydemain-id20-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844533

Dead-End Ratio: A Behavioral Model Quality Metric for Constraint-Aware Runtime Verification
Natalia Dybczak, Jagoda Flejmer, and Radosław Klimek
(AGH University of Krakow, Poland)
Automated software engineering increasingly relies on behavioral models derived from execution logs to support runtime monitoring, predictive analysis, and formal verification. However, constraints derived from such models may be unsuitable for strict runtime enforcement. We investigate this issue in constraint-aware next-event prediction and identify dead-end states, where no candidate continuation satisfies the enforced safety specification. We introduce the Dead-End Ratio (DER), which measures the proportion of observed execution prefixes admitting no valid continuation under the runtime constraint specification. Experiments on two real-world event logs yield DER values of 72.1% and 33.9%. Targeted relaxation of only a few safety rules reduces DER to 2.8% and 8.3%, respectively, while substantially restoring hard-gated predictive performance. The results show that DER provides a practical diagnostic of over-restrictive runtime specifications and supports constraint debugging before deployment.
Publisher's Version Article: asews26asydemain-id21-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844534

From Statistical Code Generation to Correct-by-Construction AI Programming: A Basis-Function Composition Framework
Yu Wu and Yuchen Yang
(Chengdu University of Technology, China; TU Munich, Germany)
Large language models have significantly advanced AI-assisted programming, but current systems still rely mainly on statistical code generation, execution feedback, testing, and human review. These mechanisms improve practical usability, yet they do not by themselves provide a construction process in which program correctness can be structurally organized, propagated, and checked. This paper presents a basis-function composition framework for correct-by-construction AI programming. The framework represents a program not merely as a sequence of generated code tokens, but as a structured composition of basis functions equipped with explicit specifications, preconditions, postconditions, and correctness evidence. Functional positions, candidate basis-function sets, hierarchical expansion, and correctness-preserving composition operators are introduced to organize automated program construction at multiple levels of abstraction. Within this framework, large language models are repositioned as assistants for specification interpretation, candidate retrieval, structural search, and code realization, rather than as the source of correctness itself. We illustrate the framework using the 0--1 knapsack problem, showing how basis-function composition supports dynamic-programming construction and helps expose semantic mismatches such as invalid update orders in space-optimized implementations. The paper argues that verifiable AI programming requires a shift from generating plausible code strings to constructing structured, interpretable, and checkable program objects.
Publisher's Version Article: asews26asydemain-id8-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844528

STAFF: Towards Translating Formal Verification Benchmarks between Formal Specification Languages
Merlijn Sevenhuijsen
(TRATON, Sweden; KTH Royal Institute of Technology, Sweden)
The development and evaluation of automated formal verification techniques for underrepresented languages are constrained by the limited availability of data. Translating existing benchmarks into such languages can reduce this fragmentation. However, differences in type systems, memory models, and verification semantics make reliable deterministic translation difficult. This paper investigates translation between formal specification languages by presenting STAFF, an automated pipeline that uses large language models to translate verified Dafny programs into ACSL-annotated C programs. STAFF validates the source file, translates its implementation and specification, and iteratively repairs faulty candidates. Finally, STAFF assesses the translation quality through five complementary checks: specification-clause matching, round-trip translation, Frama-C verification, mutation testing, and translated-test execution. We evaluate STAFF on 162 Dafny programs from the MBPP-DFY-153 benchmark using GPT-5.5. The initial translation attempt translates 113 files that formally verify against their translated ACSL specifications, increasing to 130 after three feedback iterations. The additional checks expose failure modes not detected by deductive verification alone, including changes in contract structure, surviving mutants, interface drift, and behavioral incompatibilities in translated test harnesses. These results show that automated translation between formal specification languages can produce formally verified target artifacts at a substantial success rate, while highlighting the value of complementary checks for assessing translation quality.
Publisher's Version Article: asews26asydemain-id14-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844531

Towards a Vertically Integrated Compiler Infrastructure to Improve Solver Time during Symbolic Execution
Sören Tempel and Christian Dietrich
(Technische Universität Braunschweig, Germany)
Symbolic execution is a dynamic software verification and testing technique that formally reasons about branches in a software under test using satisfiability modulo theories (SMT). This requires encoding branch conditions as logical formulas in the SMT-LIB format consumed by SMT solvers. Due to the complex semantics of modern programming languages, this transformation is conducted based on an intermediate representation (IR). To obtain this representation, prior work facilitates off-the-shelf compiler infrastructures (e.g., LLVM). Unfortunately, these established compilers are tailored to emitting program representations for fast execution on physical hardware, not for fast formal reasoning.
We propose integrating the compiler infrastructure with symbolic execution, thereby obtaining a program representation optimized for SMT solving. To explore this idea, we build upon an existing extensible IR to ease a co-design of the compiler, IR, and symbolic execution engine. We illustrate the potential of this integration by contributing conditional representation, a novel compiler transformation tailored to symbolic execution that results in a solver-efficient representation of pure functions with branches. Specifically, with conditional representation, such functions are represented as a single SMT expression, decreasing the number of solver queries while increasing per-query information. In our performed experiments, we symbolically execute real-world components from embedded operating systems and show that conditional representation reduces solver time by a geometric mean of 80%.
Publisher's Version Published Artifact Artifacts Available Article: asews26asydemain-id11-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844530

Artifacts for ASYDE'26: Towards a Vertically Integrated Compiler Infrastructure to Improve Solver Time during Symbolic Execution (doi:10.5281/zenodo.22095861): This dataset contains the files required to reproduce the evaluation results of the ASYDE'26 paper: Towards a Vertically Integrated Compiler Infrastructure to Improve Solver Time during Symbolic Execution. Specifically, it includes the files necessary to reproduce Figure 5 and 6 as well as Table 1 of the manuscript.

WanderVision: Scenario-Based GUI Testing for Smart TVs via Vision-Language Models
Sihyun Ahn, Juyeon Yoon, Taehyoung Kim, Eunki Song, and Shin Yoo
(Korea Advanced Institute of Science and Technology, Republic of Korea; LG Electronics, Republic of Korea)
Agents driven by Large Language Models (LLMs) have been applied to GUI testing to automate the process. The intrinsic text-based nature of LLMs requires the information about the on-screen GUI widgets to be provided in textual formats, which in turn necessitates the dependency on tools like Android Debug Bridge (ADB) that allows extraction of on-screen widget structures. The dependency on structured information, however, raises an important question: what can be done for GUI systems that lack such support? This paper proposes the use of Vision-Language Models (VLMs) for agentic testing of GUI systems that are neither web-based nor Android: for such GUI systems, instead of structured GUI widget information, we use screenshots and VLMs to figure out available on-screen widgets and generate click events to perform test scenarios. We implement a VLM-equipped GUI testing agent by extending DroidAgent, and evaluate its performance against native webOS apps running on LG smart TVs. When tasked with performing manually written test scenarios, the VLM-equipped version of DroidAgent shows 64.10% of success rate, fulfilling 25 out of 39 scenarios against webOS native Netflix and Youtube apps.
Publisher's Version Article: asews26asydemain-id10-p (type: Full Paper (8 pages)) doi:10.1145/3843777.3844529

Systematic Evaluation of Security Flaws in Low-Level Code Generated by LLMs
Fynn Janson, Peter Barth, and Eric Heim
(Mannheim University of Applied Sciences, Germany)
We aim to systematically evaluate low-level C/C++ code generated by LLMs. To this end, we provide an evaluation environment that uses dedicated test cases employing dynamic analysis to validate the existence of security issues. Our evaluation environment standardizes the interaction with different LLMs by providing the same context and comparable dialogue structures. The generated code is automatically compiled and executed against the manually crafted test cases and any detected security issues are logged. This provides a common experimental basis for systematically evaluating security weaknesses in LLM-generated code and enables future comparisons across models. Currently, we are targeting four LLMs with 64 different vibe coding dialogues that work against existing code as context. All examples are run nightly to capture non-deterministic behaviour. Despite preliminary results showing that LLM-generated code may be insecure when the prompt is not littered with security suggestions, the industry currently widely adopts it. Thus, insecure code is most likely to be produced when inexperienced developers embrace vibe coding.
Publisher's Version Article: asews26asydemain-id18-p (type: Short Paper (4 pages)) doi:10.1145/3843777.3844532

proc time: 0.14