SPLASH Companion '26: "Property-Based Testing of ..."
Property-Based Testing of Separation Logic Specifications
Zain K Aamer
(University of Pennsylvania, USA)
Separation logic (SL) has been a tried and tested method for specifying the behavior of heap-manipulating programs. We apply property-based testing (PBT) to these specifications for C programs, generating inputs that satisfy preconditions and checking that postconditions hold. Besides providing a specification language for testing, using SL means that PBT can act as a stepping stone towards full verification. We have previously developed tools that explore three generation techniques for SL specifications in the fragment supported by the CN verifier. Ongoing and future work develops AustenTest, a standalone tool that uses a separation-logic IR covering a larger SL fragment. AustenTest will be a publicly available, supported tool for other separation-logic verifiers to be able to use. Simultaneously, we are working on applying grammar-based fuzzing as a fourth approach to generation.
Article Search
Article: splashcomp26doc-p5-p (type: Extended Abstract) doi:10.1145/3837729.3842144
SPLASH Companion '26: "CoCoMUT: A Tool for Code-Context ..."
CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation
Alessandro Botta, Shiven Garisa, Jaya Vardhini Akurathi, Ahsanul Ameen Sabit, Trey Woodlief, and Soneya Binta Hossain
(University of Texas at Dallas, USA; Heritage High School, USA; William & Mary, USA)
Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-type information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects.
We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at type, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, type, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques.
The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99% of generated context records passed all applicable correctness checks.
Demo: https://youtu.be/RCUzkCQjG30 Artifact: https://github.com/assert-lab/CoCoMUT
Article Search
Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485
SPLASH Companion '26: "Understanding Correctness ..."
Understanding Correctness Failures in Compiler Optimization
Abdullah Al Noman and Mengfei Ren
(Baylor University, USA)
Compiler optimizations improve program performance but may break program correctness when transformations fail to preserve source level semantics. This extended abstract examines optimization introduced correctness failures in GCC through bugs reported by existing C compiler testing studies. We collect bug report metadata, recover available proof of concept programs, and manually validate each program before building the testing corpus. The current dataset contains 226 analyzed GCC bugs, including 159 bugs that are directly or partially related to optimization components. Our preliminary results show that tree optimization is the primary component involved in these failures, while wrong code is the most common failure type. These findings provide an empirical basis for an optimization oriented testing framework and a reusable test suite for improving compiler optimization correctness and reliability.
Article Search
Article: splashcomp26poster-p4-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839589
SPLASH Companion '26: "WGSLsmith: Randomised Testing ..."
WGSLsmith: Randomised Testing for the WebGPU Shading Language
Michał Andryskowski, Amber Gorzynski, Hasan Mohsin, and Alastair F. Donaldson
(Imperial College London, UK)
We present WGSLsmith, a tool for randomised testing of compilers for the WebGPU Shading Language (WGSL). Under the WebGPU API---now supported by all three major browsers---GPU programs are written in the WebGPU Shading Language (WGSL), and every implementation ships a WGSL compiler that validates shaders and translates them to platform-specific code. Because shaders may come from untrusted websites, these compilers can be exercised by arbitrary web pages, making them a security-critical target for testing. WGSLsmith generates random shaders to find compiler crashes and cross-implementation mismatches. We describe its architecture and usage, and how we have broadened its language feature coverage to keep up to date with the evolving WGSL specification and support features absent from the original design. We report on a campaign that uncovered 12 bugs (all confirmed, 8 fixed) in various parts of the WebGPU stack, and evaluate the thoroughness of WGSLsmith via coverage analysis.
Article Search
Article: splashcomp26demo-p10-p (type: Short Paper) doi:10.1145/3837729.3840486
SPLASH Companion '26: "Toward Reliable Automatic ..."
Toward Reliable Automatic Proxies for Code Comprehensibility
Erfan Arvan
(New Jersey Institute of Technology, USA)
Improving code comprehensibility requires measuring it reliably, yet no reliable automatic proxy for comprehensibility exists. Developing one requires a validated human-study baseline to test against. However, the human-study proxies used in the literature (e.g., Likert-scale ratings or response time on output-prediction tasks) have not been systematically validated either, and the construct itself lacks a standard definition. We address this foundational gap first: we introduce a conceptualization of comprehensibility based on expert agreement, construct a ground truth via the Delphi protocol, and evaluate commonly used human-study proxies against it. We find that proxies based on input--output reasoning and response time are particularly reliable, while syntax-based proxies are especially unreliable. With this validated foundation, we propose a controlled human study to test whether code verifiability---the ease with which static verification tools can analyze code---can serve as a reliable automatic proxy for comprehensibility. If verifiability alone explains comprehension difficulty well, it can be used as a standalone automatic proxy; if it only partially explains it, it becomes one signal among several in a combined automatic proxy. Beyond this study, the research agenda includes reassessing prior work in light of proxy reliability, evaluating LLM-based agents as substitutes for human participants, and developing tools that leverage reliable automatic proxies to improve code comprehensibility.
Article Search
Article: splashcomp26doc-p99-p (type: Extended Abstract) doi:10.1145/3837729.3842150
SPLASH Companion '26: "Template-Free Dynamic Invariant ..."
Template-Free Dynamic Invariant Detection
Erfan Arvan
(New Jersey Institute of Technology, USA)
Dynamic invariant detectors such as Daikon infer likely program invariants by evaluating candidate properties against execution traces. However, Daikon’s candidates are drawn from a fixed template library, which prevents it from expressing properties that involve project-specific logic or more than three variables. We present Oca, a dynamic invariant detector that uses a large language model (LLM) to propose candidates instead of deriving them from templates. LLM-proposed invariants are more expressive, but their integration into a dynamic analysis pipeline raises non-trivial research challenges involving prompt design, context selection, and safe execution of untrusted candidates. We address these challenges and evaluate Oca on the Defects4J benchmark, showing that it infers invariants beyond Daikon’s expressive reach, with ongoing evaluation of their bug-detection capability in property-based testing.
Article Search
Article: splashcomp26src-p13-p (type: Extended Abstract) doi:10.1145/3837729.3839576
SPLASH Companion '26: "Single-Metric Size and Complexity ..."
Single-Metric Size and Complexity Thresholds Fail to Forecast Refactoring
Binamra Aryal
(University of Texas at Arlington, USA)
Code smells, like excessive size or complexity, surface as technical debt. Static analysers flag them when metrics cross fixed thresholds rather than learning from developer behaviour. We ask whether these thresholds match where developers refactor. Adopting a revealed-preference view, we mine five Java systems, track files across renames, and learn per-metric thresholds from past refactorings. We test these blind against tool defaults and a naive median under abundant, scarce, and forecasting scenarios. Results are consistently negative: no single size or complexity metric usefully separates refactored from untouched files, and even the best comes nowhere near usable precision. Re-tuning does not help: the calibrated threshold, the default, and a naive median all sit in the same low range. The default thresholds are miscalibrated, but the single-metric premise fails for size and complexity.
Article Search
Article: splashcomp26src-p4-p (type: Extended Abstract) doi:10.1145/3837729.3839569
SPLASH Companion '26: "Knowing When a Cheap Model ..."
Knowing When a Cheap Model Is Enough: An Information Limit on Pre-review Cost Routing for LLM Code Review
Md Khairul Azman
(Texas State University, USA)
Large language models now review code at scale, but sending every pull request to a single frontier model is wasteful: many changes are reviewed as well by a far cheaper one. Cost routing has produced large savings for code generation, where an executable oracle checks quality; review instead answers to a human maintainer, and the cost of a missed defect is uneven. We ask whether routing can deliver the same savings here. On 601 real pull requests, across an open-source and a closed-source two-tier pair, the opportunity is present but moderate: the cheap model reaches 90% of the strong model's coverage on 48 to 51% of requests, and an oracle that down-routes those requests cuts cost by 38 to 49% without losing coverage. Yet the opportunity cannot be captured in advance: whether a request is safe to down-route is predictable at little better than chance from pull-request metadata, human difficulty labels, and the cheap model's own review, with every channel at AUC 0.55 or below. The limit is one of information, not model capacity: economical review should spend on the review, not on forecasting its difficulty.
Article Search
Article: splashcomp26src-p24-p (type: Extended Abstract) doi:10.1145/3837729.3839585
SPLASH Companion '26: "Code as Interface for No-Code ..."
Code as Interface for No-Code
Niv Benaloul
(Open University of Israel, Israel)
Can the code that a no-code platform generates serve as a debugging interface rather than a hidden implementation detail? This research investigates that question for block-based no-code development, where a single visual program is compiled to several target languages whose runtime semantics can diverge without being visible at the block level. The premise is that these divergences are observable evidence to be surfaced, not defects to normalize away.
To illustrate this, we present glassbox debugging, a model that sits between blackbox (visual-only) and whitebox (code-only) approaches, and evaluate it through a proof-of-concept tool, Glancer, and a diagnostic-coverage study over eight curated Blockly programs, in which the exposed code makes the source-level cause observable in all eight cross-language fault classes while a blackbox-only baseline reveals none.
Article Search
Article: splashcomp26src-p25-p (type: Extended Abstract) doi:10.1145/3837729.3839586
SPLASH Companion '26: "Measuring Per-Decision Propagation ..."
Measuring Per-Decision Propagation Work as a Formula-Dependent Signal
Zenas Boamah
(Haverford College, USA)
Hardware accelerators for Boolean satisfiability (SAT) target the solver's inner loop, Boolean constraint propagation (BCP). Every offload carries a fixed overhead, so what decides whether acceleration pays is the work delivered per invocation. For a conflict-driven clause-learning (CDCL) solver the natural unit of that work is the propagation rate (PR): propagations per decision. Across seven SATLIB families and 5,199 instances, PR varies roughly fivefold, and is captured neither by the clause-to-variable ratio, the standard predictor of SAT hardness, nor by formula size alone: families matched on size still differ more than twofold. On 210 industrial instances it spans two orders of magnitude across application domains, and within five of them it can be estimated before solving, from the formula's community structure alone. PR is a trace statistic of little use to a software solver; it does not change how the solver runs, but under hardware acceleration it determines whether a formula carries enough work per offload to justify sending it at all.
Article Search
Article: splashcomp26src-p19-p (type: Extended Abstract) doi:10.1145/3837729.3839581
SPLASH Companion '26: "Modular Abstract Interpretation ..."
Modular Abstract Interpretation for Stack-Heap Analysis of C/C++ via LLVM IR
Giacomo Boldini
(Ca' Foscari University of Venice, Italy)
Detecting memory errors in C/C++ by static analysis means reasoning about program values and memory structure together, but value- and memory-oriented analyses are usually combined in fixed, domain-specific ways. This work proposes a modular, parametric framework, based on abstract interpretation theory, with a split-state abstraction that separates values from memory structure into two independent, interchangeable domains. Any pair satisfying a minimal interface yields a sound combined analysis by construction. Precision can thus be adapted without redesigning the analysis, for instance by trading a coarser memory domain for a richer value one.
Article Search
Article: splashcomp26src-p9-p (type: Extended Abstract) doi:10.1145/3837729.3839572
SPLASH Companion '26: "How Far Does Replication Pay ..."
How Far Does Replication Pay Off? A Throughput-Area Study of Brute-Force SAT on an ECP5 FPGA
Andrew Bonilla
(Columbia University, USA)
SAT solving is a core computational challenge across hardware verification, electronic design, and planning; an FPGA can evaluate SAT candidates at hardware clock rates without software overhead, enabling sub-microsecond solving on small instances. Yet, the throughput-area tradeoffs of parallel FPGA SAT datapaths remain undercharacterized on open-source toolchains. We implement a brute-force SAT solver on a Lattice ECP5 FPGA using Amaranth HDL, Yosys, and nextpnr, and characterize K-way candidate-level parallelism: replicating the clause-evaluation datapath K times to test K candidate solutions in parallel per clock cycle. Across K=1–128, cycle reduction is near-ideal (123.81× at K=128), while real speedup (37.37×) is bounded primarily by fmax degradation from the deepening winner-selection network. Throughput efficiency and area efficiency diverge: fmax retention falls monotonically while speedup per LUT rises, peaks near 8.22×10−4 at K=64, then declines as LUT cost outpaces speedup gain. Static timing analysis identifies the winner-selection network as the dominant timing bottleneck, with routing contributing ∼80% of critical-path delay at K=64.
Article Search
Article: splashcomp26src-p15-p (type: Extended Abstract) doi:10.1145/3837729.3839578
SPLASH Companion '26: "CoCoMUT: A Tool for Code-Context ..."
CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation
Alessandro Botta, Shiven Garisa, Jaya Vardhini Akurathi, Ahsanul Ameen Sabit, Trey Woodlief, and Soneya Binta Hossain
(University of Texas at Dallas, USA; Heritage High School, USA; William & Mary, USA)
Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-type information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects.
We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at type, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, type, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques.
The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99% of generated context records passed all applicable correctness checks.
Demo: https://youtu.be/RCUzkCQjG30 Artifact: https://github.com/assert-lab/CoCoMUT
Article Search
Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485
SPLASH Companion '26: "ADEPT: A Unified Framework ..."
ADEPT: A Unified Framework for Deep Learning Test Adequacy
Yidi Kao, Shawn Burnham, Tommi Rose Fahy, and Ali Ghanbari
(Auburn University, USA)
Over the past decade, many test adequacy metrics have been proposed for deep learning that characterize test dataset adequacy from different perspectives, e.g., neuron activation behavior, latent feature coverage, decision-boundary exploration, etc. However, these metrics are typically released as independent research prototypes with substantially different installation and preprocessing requirements, execution workflows, and configuration mechanisms. These complications make them quite difficult to reproduce, compare, and adopt in research work and practical deployment alike. In this paper, we present the engineering details of ADEPT, a framework that integrates representative adequacy techniques, including neuron-coverage-based metrics, surprise adequacy, input distribution coverage, boundary coverage, and source- and model-level mutation score, under a consistent execution workflow. ADEPT provides a template-based metric interface with well-defined extension points for integrating new adequacy metrics. Furthermore, it provides YAML-based configuration management, preprocessing-cache reuse, and structured result reporting, making it easy to use in any research and development workflows. ADEPT is designed for researchers and practitioners who wish to reproduce and apply adequacy metrics without spending days or weeks implementing missing tooling or configuring disparate research prototypes. A demo video is available at https://aub.ie/ADEPT_video.
Article Search
Article: splashcomp26demo-p14-p (type: Short Paper) doi:10.1145/3837729.3840488
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "Bridging Call Boundaries: ..."
Bridging Call Boundaries: Inter-procedural Semantic Completion for Graph-Based Vulnerability Detection
Ruiguo Hu, Dongqi Wang, Shujin Yang, Zhenglin Li, and Dongming Chen
(Northeastern University, China)
Deep learning-based vulnerability detection approaches are limited when vulnerabilities involve multiple functions, where the security effect of a function depends on the behavior of invoked functions. As a result, function-level models may miss key vulnerability-related information across call boundaries. To address this issue, we propose VulSCG, a graph-based vulnerability detection framework with inter-procedural semantic completion. VulSCG first retrieves callee implementations from the corresponding project version and uses LLMs to generate structured summaries of their input, output and security-relevant behaviors. The generated summaries are injected into the caller Code Property Graph as SummaryNodes, allowing inter-procedural security semantics to participate in graph learning without expanding the full callee graph. Experiments on Devign show that VulSCG outperforms representative learning-based vulnerability detection baselines. In particular, VulSCG achieves the best F1 score on the dataset, with a F1 improvement of 4.25% over the strongest baseline. These results indicate that VulSCG improves detection effectiveness while maintaining scalability, since it complements inter-procedural semantics through compact SummaryNodes rather than full callee graph expansion.
Article Search
Article: splashcomp26poster-p5-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839590
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Towards Scalable and Verifiable ..."
Towards Scalable and Verifiable Automated Translation from C to Safe Rust
Victor Chen
(Ohio State University, USA)
Memory-safety bugs are one of the oldest and most common sources of security vulnerabilities, and their modern-day prevalence is a consequence of the widespread use of non-memory-safe languages such as C and C++. Transitioning away from C and C++ to memory-safe languages, namely Rust, to eliminate memory-safety bugs is growing in popularity as a potential solution, but manual migration of the vast C/C++ codebases in deployment to Rust is hardly practical.
This thesis proposes an approach to verifiable automated translation from C to safe Rust that scales to real-world software. By introducing new tools and techniques for reasoning about Rust types, correctness, rewriting, verification, and testing tailored to C-to-Rust translation, this work will show that automated translation from C to Rust that both "does the right thing" is comparable in quality to code written by an experienced Rust developer is possible.
Article Search
Article: splashcomp26doc-p96-p (type: Extended Abstract) doi:10.1145/3837729.3842149
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Falconf: A Web-Based Tool ..."
Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis
Youyang Kim, Sahil Suneja, Yong-Hwan Jeong, Yunja Choi, Young-Woo Kwon, and Byungchul Tak
(Kyungpook National University, Republic of Korea; IBM Research, USA)
Misconfigurations continue to be one of the major causes of failures in distributed software systems, yet diagnosing them remains challenging. This is because faulty configuration parameters are difficult to identify among hundreds of configuration entries, and their effects often leave no explicit evidence in runtime logs. We present Falconf, a web-based tool for automatically diagnosing misconfigurations in distributed software systems using log analysis. Falconf takes runtime log files as input, analyzes them using a pre-trained two-stage transformer model, and produces a ranked list of suspicious configuration parameters that are likely responsible for the observed failure. The tool features an intuitive web interface that visualizes the diagnosis workflow, allowing users to select the target application and version, input log files, and inspect the ranked results without any expertise in machine learning or log analysis. We demonstrate that Falconf can effectively diagnose misconfigured parameters from real-world logs of distributed software systems, including Apache Spark and Hadoop.
Article Search
Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499
SPLASH Companion '26: "Slice-Guided, Context-Augmented ..."
Slice-Guided, Context-Augmented Large Language Model Inference of Java Nullability Annotations
Mushfiqur Rahman Chowdhury
(New Jersey Institute of Technology, USA)
Java nullness checkers such as NullAway catch potential null-pointer errors, but adopting them on legacy code is difficult. Most projects lack complete nullability annotations, and existing tools such as NullAwayAnnotator are checker- specific and can still leave warnings behind. We present a warning-guided, slice-based, LLM-assisted pipeline for inferring Java nullability annotations. It first runs NullAway to locate the warnings, then uses Specimin, a type-directed slicer that extracts the minimum compilable code needed to reproduce a warning, to build a small slice around each warning-relevant method or field. It augments the prompt with usage context. The model gets two complementary inputs, the compilable slice and this textual evidence, and infers the annotations @Nullable and @Nonnull without touching program logic. Annotations are merged back, re-checked, and a post-processing loop fixes whatever still triggers a warning. On EventBus, where NullAwayAnnotator leaves 11 warnings unresolved, our pipeline resolves all warnings. We see this checker-guided design as a step toward a type-system-independent inference technique.
Article Search
Article: splashcomp26src-p21-p (type: Extended Abstract) doi:10.1145/3837729.3839583
SPLASH Companion '26: "Diffpoints: Breakpoints Comparing ..."
Diffpoints: Breakpoints Comparing Values of Variables
Filip Čmilňák, Matúš Sulír, and Milan Nosáľ
(Technical University of Košice, Slovakia; ValeSoft, Slovakia)
Debugging is an integral, yet time-consuming and cognitively demanding part of software development. While common debugging tools allow for a detailed inspection of current variable values, they do not offer a clear visualization of their evolution over time. When comparing states at different execution points, they rely on the programmer’s memory or auxiliary console outputs. In this paper, we present Diffpoints, a novel debugging tool that introduces new types of breakpoints to enable the automatic capture and comparison of variable states between multiple points of program execution. Two distinct types, namely line and group diffpoints, are supported, and to match variables from different stack traces, a heuristic is used. Diffpoints are implemented as an extension for the IntelliJ IDEA development environment. We conducted a preliminary user study and plan further evaluation.
Article Search
Article: splashcomp26demo-p35-p (type: Short Paper) doi:10.1145/3837729.3840495
SPLASH Companion '26: "SiRL: Signal-Level Reinforcement ..."
SiRL: Signal-Level Reinforcement Learning for Falsifying Cyber-Physical Systems
Hadiza Yusuf, Khouloud Gaaloul, and Aditi Dharmadhikari
(University of Michigan at Dearborn, USA)
Temporal logic falsification searches for inputs that cause a Cyber-Physical System to violate a Signal Temporal Logic property. Existing deep reinforcement learning (DRL) methods frame falsification as a sequential decision problem where the agent selects one input value per simulation timestep. We propose SiRL, a signal-level DRL approach that selects a complete input trajectory per simulation step and learns from the full history of interactions. Evaluated on 12 requirements of two benchmarks against two baselines, SiRL achieves the highest falsification rate on 9 of 12 benchmarks and is the only tool to falsify one unique case, while also achieving the lowest per-simulation wall-clock time across all tools.
Article Search
Article: splashcomp26poster-p3-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839588
SPLASH Companion '26: "Iekkë: A Bounded-Round Partial-Order ..."
Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, and Gennaro Parlato
(Gran Sasso Science Institute, Italy; Stellenbosch University, South Africa; University of Salerno, Italy; Diffblue, UK; University of Molise, Italy)
We present Iekkë, a BMC tool for verifying multi-threaded C programs. It implements a new bounded-round partial-order encoding for the sequential consistency shared-memory model. The encoding combinesbthe compactness of lazy sequentialization with the structural precision of the partial-order approach. Its concurrency constraints grow linearly in the number of shared-memory events and in the round bound 𝑘—--avoiding the quadratic/cubic blow-up of classical partial-order encodings—--and are fully propositional, enabling the use of an off-the-shelf SAT solver. Iekkë is built on top of the CBMC/Deagle infrastructure and replaces only the concurrency constraint module. It supports concurrent reachability checking, data race detection, and the usual safety property checks implemented by CBMC. Iekkë won the Bronze medal in the Concurrency category of SV-COMP 2026.
Article Search
Article: splashcomp26demo-p18-p (type: Short Paper) doi:10.1145/3837729.3840491
SPLASH Companion '26: "WGSLsmith: Randomised Testing ..."
WGSLsmith: Randomised Testing for the WebGPU Shading Language
Michał Andryskowski, Amber Gorzynski, Hasan Mohsin, and Alastair F. Donaldson
(Imperial College London, UK)
We present WGSLsmith, a tool for randomised testing of compilers for the WebGPU Shading Language (WGSL). Under the WebGPU API---now supported by all three major browsers---GPU programs are written in the WebGPU Shading Language (WGSL), and every implementation ships a WGSL compiler that validates shaders and translates them to platform-specific code. Because shaders may come from untrusted websites, these compilers can be exercised by arbitrary web pages, making them a security-critical target for testing. WGSLsmith generates random shaders to find compiler crashes and cross-implementation mismatches. We describe its architecture and usage, and how we have broadened its language feature coverage to keep up to date with the evolving WGSL specification and support features absent from the original design. We report on a campaign that uncovered 12 bugs (all confirmed, 8 fixed) in various parts of the WebGPU stack, and evaluate the thoroughness of WGSLsmith via coverage analysis.
Article Search
Article: splashcomp26demo-p10-p (type: Short Paper) doi:10.1145/3837729.3840486
SPLASH Companion '26: "Dredd: Scalable Source-Level ..."
Dredd: Scalable Source-Level Mutation Testing for Large C/C++ Codebases
Alastair F. Donaldson, James Lee-Jones, and Jonathan Foo
(Imperial College London, UK)
We present Dredd, a new tool that supports source-level mutation testing for large C/C++ codebases. Following the mutant schemata approach, Dredd applies a source-to-source transformation to a chosen set of files from the system under test (SUT), rewriting them into a metamutant that simulates a large number of distinct mutants, each selected via an environment variable holding the desired mutant’s ID. With no mutant selected, the metamutant behaves like the original SUT; otherwise it behaves as if a specific edit—such as replacing a binary operator or deleting a statement—had been applied. Because the metamutant is compiled and linked only once, mutation analysis across many mutants avoids expensive per-mutant recompilation and linking. We evaluate Dredd’s scalability on the Clang/LLVM compiler (a large C++ project) and the zstd compression library (a sizeable C project), and showcase an application of Dredd in compiler testing, using it to compare how effective the Csmith and YARPGen v1 and v2 tools are at killing mutants in Clang/LLVM.
Article Search
Article: splashcomp26demo-p6-p (type: Short Paper) doi:10.1145/3837729.3840482
SPLASH Companion '26: "The Mechanisms and Practice ..."
The Mechanisms and Practice of Mutation Testing in Improving Software Quality
Hang Du
(University of California at Irvine, USA)
Mutation testing has been studied for over four decades as a technique for assessing and improving test suites, yet important questions remain about why it works, whether killing surviving mutants improves real-fault detection, and how developers use it in practice. This proposed dissertation investigates mutation testing from three complementary perspectives. First, it examines how mutations interact with program executions and test oracles to produce mutant kills and reveal opportunities for test improvement. Second, it studies whether killing individual surviving mutants can help expose real bugs and through what mechanisms. Third, it investigates how mutation testing is adopted, configured, sustained, and acted upon in popular open-source projects.
Article Search
Article: splashcomp26doc-p57-p (type: Extended Abstract) doi:10.1145/3837729.3842147
SPLASH Companion '26: "ADEPT: A Unified Framework ..."
ADEPT: A Unified Framework for Deep Learning Test Adequacy
Yidi Kao, Shawn Burnham, Tommi Rose Fahy, and Ali Ghanbari
(Auburn University, USA)
Over the past decade, many test adequacy metrics have been proposed for deep learning that characterize test dataset adequacy from different perspectives, e.g., neuron activation behavior, latent feature coverage, decision-boundary exploration, etc. However, these metrics are typically released as independent research prototypes with substantially different installation and preprocessing requirements, execution workflows, and configuration mechanisms. These complications make them quite difficult to reproduce, compare, and adopt in research work and practical deployment alike. In this paper, we present the engineering details of ADEPT, a framework that integrates representative adequacy techniques, including neuron-coverage-based metrics, surprise adequacy, input distribution coverage, boundary coverage, and source- and model-level mutation score, under a consistent execution workflow. ADEPT provides a template-based metric interface with well-defined extension points for integrating new adequacy metrics. Furthermore, it provides YAML-based configuration management, preprocessing-cache reuse, and structured result reporting, making it easy to use in any research and development workflows. ADEPT is designed for researchers and practitioners who wish to reproduce and apply adequacy metrics without spending days or weeks implementing missing tooling or configuring disparate research prototypes. A demo video is available at https://aub.ie/ADEPT_video.
Article Search
Article: splashcomp26demo-p14-p (type: Short Paper) doi:10.1145/3837729.3840488
SPLASH Companion '26: "CrossLangFuzzer: Differential ..."
CrossLangFuzzer: Differential Testing of Cross-Language JVM Compilers
Xiaotian Ma, Qiong Feng, Yongqiang Tian, Wei Song, and Peng Liang
(Nanjing University of Science and Technology, China; Monash University, Australia; Wuhan University, China)
Modern JVM software increasingly integrates multiple programming languages, such as Java, Kotlin, Groovy, and Scala, within a single application. Supporting such interoperability requires JVM compilers to perform cross-language compilation while reconciling subtle semantic differences across language boundaries. Errors in this process can lead to critical miscompilations, yet existing compiler testing techniques focus exclusively on isolated, single-language compilation. To address this gap, we present CrossLangFuzzer, the first differential testing framework for cross-language JVM compilation. CrossLangFuzzer leverages the Kotlin compiler's unified intermediate representation (IR) to synthesize cross language test programs. It further applies seven mutation operators to diversify generated test programs and improve bug-finding capability. Evaluated on the latest versions of five major JVM compilers, CrossLangFuzzer uncovered 32 confirmed bugs, including 15 in Kotlin, 4 in Groovy, 7 in Scala 3, 2 in Scala 2, and 4 in Java.
Article Search
Article: splashcomp26demo-p21-p (type: Short Paper) doi:10.1145/3837729.3840493
SPLASH Companion '26: "Iekkë: A Bounded-Round Partial-Order ..."
Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, and Gennaro Parlato
(Gran Sasso Science Institute, Italy; Stellenbosch University, South Africa; University of Salerno, Italy; Diffblue, UK; University of Molise, Italy)
We present Iekkë, a BMC tool for verifying multi-threaded C programs. It implements a new bounded-round partial-order encoding for the sequential consistency shared-memory model. The encoding combinesbthe compactness of lazy sequentialization with the structural precision of the partial-order approach. Its concurrency constraints grow linearly in the number of shared-memory events and in the round bound 𝑘—--avoiding the quadratic/cubic blow-up of classical partial-order encodings—--and are fully propositional, enabling the use of an off-the-shelf SAT solver. Iekkë is built on top of the CBMC/Deagle infrastructure and replaces only the concurrency constraint module. It supports concurrent reachability checking, data race detection, and the usual safety property checks implemented by CBMC. Iekkë won the Bronze medal in the Concurrency category of SV-COMP 2026.
Article Search
Article: splashcomp26demo-p18-p (type: Short Paper) doi:10.1145/3837729.3840491
SPLASH Companion '26: "Dredd: Scalable Source-Level ..."
Dredd: Scalable Source-Level Mutation Testing for Large C/C++ Codebases
Alastair F. Donaldson, James Lee-Jones, and Jonathan Foo
(Imperial College London, UK)
We present Dredd, a new tool that supports source-level mutation testing for large C/C++ codebases. Following the mutant schemata approach, Dredd applies a source-to-source transformation to a chosen set of files from the system under test (SUT), rewriting them into a metamutant that simulates a large number of distinct mutants, each selected via an environment variable holding the desired mutant’s ID. With no mutant selected, the metamutant behaves like the original SUT; otherwise it behaves as if a specific edit—such as replacing a binary operator or deleting a statement—had been applied. Because the metamutant is compiled and linked only once, mutation analysis across many mutants avoids expensive per-mutant recompilation and linking. We evaluate Dredd’s scalability on the Clang/LLVM compiler (a large C++ project) and the zstd compression library (a sizeable C project), and showcase an application of Dredd in compiler testing, using it to compare how effective the Csmith and YARPGen v1 and v2 tools are at killing mutants in Clang/LLVM.
Article Search
Article: splashcomp26demo-p6-p (type: Short Paper) doi:10.1145/3837729.3840482
SPLASH Companion '26: "SiRL: Signal-Level Reinforcement ..."
SiRL: Signal-Level Reinforcement Learning for Falsifying Cyber-Physical Systems
Hadiza Yusuf, Khouloud Gaaloul, and Aditi Dharmadhikari
(University of Michigan at Dearborn, USA)
Temporal logic falsification searches for inputs that cause a Cyber-Physical System to violate a Signal Temporal Logic property. Existing deep reinforcement learning (DRL) methods frame falsification as a sequential decision problem where the agent selects one input value per simulation timestep. We propose SiRL, a signal-level DRL approach that selects a complete input trajectory per simulation step and learns from the full history of interactions. Evaluated on 12 requirements of two benchmarks against two baselines, SiRL achieves the highest falsification rate on 9 of 12 benchmarks and is the only tool to falsify one unique case, while also achieving the lowest per-simulation wall-clock time across all tools.
Article Search
Article: splashcomp26poster-p3-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839588
SPLASH Companion '26: "OLIVE: Output-Level Iterative ..."
OLIVE: Output-Level Iterative Verification Engine
Aila Jahromi, Junhao Gao, Zhixuan He, and Jonathan Mendoza
(University of California at San Diego, USA)
Large language models (LLMs) can effectively generate action plans from natural-language descriptions but provide no guarantees that their outputs satisfy domain-specific safety requirements. This limitation is particularly concerning in safety-critical domains such as emergency medicine, where protocol violations can jeopardize patient safety. We present OLIVE, a framework that combines LLM-generated plans with automated repair to automatically generate medical procedures with formally verified safety guarantees. OLIVE encodes established medical safety protocols as logical constraints in the Alloy specification language and verifies candidate plans against them. When verification identifies protocol violations, OLIVE incorporates the resulting counterexample directly into the generation loop to iteratively repair the candidate plan while preserving the LLM’s context-sensitive reasoning. We evaluate OLIVE on emergency medical scenarios derived from established clinical protocols and demonstrate that it automatically repairs protocol violations to produce plans that satisfy all specified safety requirements.
Article Search
Article: splashcomp26src-p3-p (type: Extended Abstract) doi:10.1145/3837729.3839568
SPLASH Companion '26: "OmniJinja: A Cross-Language ..."
OmniJinja: A Cross-Language VS Code Extension for Jinja Application Development
Yu Sun, Kai Gao, and Chang-ai Sun
(University of Science and Technology Beijing, China)
Jinja is one of the most widely used template engines in the Python ecosystem, enabling applications to generate documents by combining dynamic data with templates. Jinja application development is challenging because templates are polyglot artifacts and interact with backend code through implicit cross-language data contracts. However, existing tools provide limited assistance for maintaining consistency between the backend and templates. In this paper, we present OmniJinja, an event-driven VS Code extension for Jinja application development. OmniJinja performs cross-language analysis of backend Python code and Jinja templates to provide backend-aware completion, bidirectional consistency checking, and syntax diagnostics with quick fixes. A lightweight evaluation on three real-world Jinja projects demonstrates that OmniJinja effectively provides backend-aware completion and detects cross-language inconsistencies.
Article Search
Article: splashcomp26demo-p17-p (type: Short Paper) doi:10.1145/3837729.3840490
SPLASH Companion '26: "CoCoMUT: A Tool for Code-Context ..."
CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation
Alessandro Botta, Shiven Garisa, Jaya Vardhini Akurathi, Ahsanul Ameen Sabit, Trey Woodlief, and Soneya Binta Hossain
(University of Texas at Dallas, USA; Heritage High School, USA; William & Mary, USA)
Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-type information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects.
We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at type, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, type, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques.
The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99% of generated context records passed all applicable correctness checks.
Demo: https://youtu.be/RCUzkCQjG30 Artifact: https://github.com/assert-lab/CoCoMUT
Article Search
Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485
SPLASH Companion '26: "ADEPT: A Unified Framework ..."
ADEPT: A Unified Framework for Deep Learning Test Adequacy
Yidi Kao, Shawn Burnham, Tommi Rose Fahy, and Ali Ghanbari
(Auburn University, USA)
Over the past decade, many test adequacy metrics have been proposed for deep learning that characterize test dataset adequacy from different perspectives, e.g., neuron activation behavior, latent feature coverage, decision-boundary exploration, etc. However, these metrics are typically released as independent research prototypes with substantially different installation and preprocessing requirements, execution workflows, and configuration mechanisms. These complications make them quite difficult to reproduce, compare, and adopt in research work and practical deployment alike. In this paper, we present the engineering details of ADEPT, a framework that integrates representative adequacy techniques, including neuron-coverage-based metrics, surprise adequacy, input distribution coverage, boundary coverage, and source- and model-level mutation score, under a consistent execution workflow. ADEPT provides a template-based metric interface with well-defined extension points for integrating new adequacy metrics. Furthermore, it provides YAML-based configuration management, preprocessing-cache reuse, and structured result reporting, making it easy to use in any research and development workflows. ADEPT is designed for researchers and practitioners who wish to reproduce and apply adequacy metrics without spending days or weeks implementing missing tooling or configuring disparate research prototypes. A demo video is available at https://aub.ie/ADEPT_video.
Article Search
Article: splashcomp26demo-p14-p (type: Short Paper) doi:10.1145/3837729.3840488
SPLASH Companion '26: "WGSLsmith: Randomised Testing ..."
WGSLsmith: Randomised Testing for the WebGPU Shading Language
Michał Andryskowski, Amber Gorzynski, Hasan Mohsin, and Alastair F. Donaldson
(Imperial College London, UK)
We present WGSLsmith, a tool for randomised testing of compilers for the WebGPU Shading Language (WGSL). Under the WebGPU API---now supported by all three major browsers---GPU programs are written in the WebGPU Shading Language (WGSL), and every implementation ships a WGSL compiler that validates shaders and translates them to platform-specific code. Because shaders may come from untrusted websites, these compilers can be exercised by arbitrary web pages, making them a security-critical target for testing. WGSLsmith generates random shaders to find compiler crashes and cross-implementation mismatches. We describe its architecture and usage, and how we have broadened its language feature coverage to keep up to date with the evolving WGSL specification and support features absent from the original design. We report on a campaign that uncovered 12 bugs (all confirmed, 8 fixed) in various parts of the WebGPU stack, and evaluate the thoroughness of WGSLsmith via coverage analysis.
Article Search
Article: splashcomp26demo-p10-p (type: Short Paper) doi:10.1145/3837729.3840486
SPLASH Companion '26: "Safe<T>: Automaton-Theoretic ..."
Safe<T>: Automaton-Theoretic Runtime Monitoring of Blackbox Distributed Systems
Karuna Grewal
(Cornell University, USA)
Modern safety-critical systems are increasingly built from blackbox components: cloud services, third-party APIs, autonomous systems, and AI agents whose source code or internal state may be unavailable for inspection. To certify safe and secure inter-component interactions in such systems, security and compliance teams must enforce policies over sequential and nested call/return patterns in the execution, along with the data values exchanged between the components. Furthermore, the blackbox setting necessitates decoupling the policy enforcement mechanism from the system implementation. To this end, I design Safe⟨ T⟩, an automaton-theoretic runtime monitoring framework for specifying and enforcing control-flow and data-aware policies over black-box distributed systems. My technique is blackbox and non-invasive, i.e., it requires no code access or implementation changes. To realize this framework, I have built a distributed runtime monitor on top of an emerging network infrastructure layer that can control inter-component communication. I have demonstrated Safe⟨ T⟩ on cloud microservices and am now extending it to agentic AI systems.
Article Search
Article: splashcomp26doc-p86-p (type: Extended Abstract) doi:10.1145/3837729.3842148
SPLASH Companion '26: "Phoenix: A Modular and Versatile ..."
Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis
Peisen Yao, Zinan Gu, and Qingkai Shi
(Zhejiang University, China; Nanjing University, China)
We present Phoenix, a modular pointer analysis framework for C/C++ that unifies multiple alias analysis algorithms behind a single, stable interface. Phoenix addresses the fragmentation of today’s C/C++ pointer analysis ecosystem by cleanly separating IR construction, constraint generation, solver backends, and client-facing queries—making analyses easy to compare, swap, and compose while exposing explicit precision–performance trade-offs. We evaluate two comparisons on 28 GNU coreutils programs: Phoenix-FICI versus SVF-FICI, where both analyses are flow-insensitive and context-insensitive, and Phoenix-FSCS versus SVF-FSCI, where the former is flow- and context-sensitive and the latter is flow-sensitive but context-insensitive. Phoenix-FICI is faster on all benchmarks, with a maximum speedup of 2.88×. For the second comparison, Phoenix-FSCS is faster on 13 benchmarks, slower on 14, and tied on one, with a maximum speedup of 2.91×. In production, Phoenix serves as the analysis substrate for static analysis and fuzzing tools that have uncovered hundreds of new bugs in open-source software and industrial deployments.
Article Search
Article: splashcomp26demo-p19-p (type: Short Paper) doi:10.1145/3837729.3840492
SPLASH Companion '26: "HeapLens: An IDE-Integrated ..."
HeapLens: An IDE-Integrated Tool for Heap Dump Analysis with In-Editor Source Bridging and LLM-Assisted Diagnosis
Sachin Gupta
(Independent, USA)
We present HeapLens, an open-source VS Code extension that brings Java heap dump analysis into the editor. HeapLens pairs a Rust backend (memory-mapped HPROF parsing, a Compressed Sparse Row reference graph, Lengauer–Tarjan dominator computation, and a HeapQL query engine) with an eleven-view webview UI that integrates heap analysis into the developer’s source workspace. The tool exposes jump-to-source navigation that links each retained class to its Java declaration through the editor’s workspace file index, and an LLM-assisted diagnosis panel that supports ten language model providers including a local Ollama backend for sensitive heaps. On the largest dump we evaluate (14.8 GB), HeapLens completes a full analysis in 9.5 seconds with a 21 GB peak resident set, without writing disk indices. HeapLens has accumulated over 2,900 installs across the VS Code Marketplace and the Open VSX Registry, which serves Cursor, Windsurf, Codespaces, VSCodium, and similar IDE forks. The tool is released under Apache 2.0 and archived on Zenodo.
Article Search
Article: splashcomp26demo-p1-p (type: Short Paper) doi:10.1145/3837729.3840479
SPLASH Companion '26: "ActionTaint: Framework-Aware ..."
ActionTaint: Framework-Aware Taint Analysis for Next.js Server Actions
Aisha Gurbanli
(Azerbaijan State University of Economics, Azerbaijan)
Next.js Server Actions simplify full-stack application development by allowing server-side functions to be called directly from UI components. While these functions may appear as regular JavaScript functions, the framework can expose them as client-accessible server endpoints, creating hidden trust boundaries that are invisible to traditional static analysis. As a result, existing JavaScript analyzers often fail to recognize Server Action inputs as client-accessible, leading to missed security flows that are embedded in the source.
This paper introduces ActionTaint, a framework-based static analysis prototype that reconstructs client-accessible Server Actions, models them as explicit client-server trust boundaries, and automatically generates CodeQL taint specifications. Rather than implementing a new taint engine, ActionTaint serves as a semantic adapter between the Next.js framework semantics and CodeQL's inter-procedural taint analysis. Evaluation on synthetic benchmarks, project-like benchmarks, real open-source applications, and seeded vulnerability experiments shows that Server Action's open access modeling allows for the detection of SQL injection, SSRF, path traversal, open redirection, and authorization-related flows that are not visible in standard CodeQL.
Article Search
Article: splashcomp26src-p12-p (type: Extended Abstract) doi:10.1145/3837729.3839575
SPLASH Companion '26: "Can We Trust RefAgent? A Differential-Fuzzing ..."
Can We Trust RefAgent? A Differential-Fuzzing Test of Functional Equivalence in Multi-agent-Based Java Refactoring
Mustahid Hasan
(William & Mary, USA)
Multi-agent LLM frameworks such as RefAgent report state-of-the-art results for automatic Java refactoring, validated through compilation success, unit-test pass rates, and code-smell reduction. None of these efforts, however, establishes the property that defines a refactoring: behavior preservation. This report therefore asks whetherRefAgent’s refactorings are semantically correct, and we answer in two steps. First, we reproduced RefAgent and regenerated its refactored corpus on two large Apache projects since the original artifact released neither the refactored code nor an executable pipeline. Second, after generating the refactored corpus, we audited the corpus with coverage-guided differential fuzzing: Jazzer drives automatically generated inputs through both versions of each method and reports a counterexample whenever they disagree on an observable outcome. Our results show that, across 371 auto-fuzzable methods from Apex Core and JMeter, 28.57% and 11.83% of methods, respectively, diverged, and no existing test in either project covers the divergent behavior. To our knowledge, this is the first behavior-preservation audit of a multi-agent LLM refactoring framework whose refactored corpus has already passed compile-and-test checks. Test-pass and smell-reduction metrics therefore overstate the trustworthiness of agent-assisted refactoring, and differential fuzzing supplies the low-cost oracle they miss.
Article Search
Article: splashcomp26src-p22-p (type: Extended Abstract) doi:10.1145/3837729.3839584
SPLASH Companion '26: "ThunderFork: Splitting SMT ..."
ThunderFork: Splitting SMT Queries with Targeted Control-Flow Transformations
Muhammad Hassan
(Virginia Tech, USA)
SMT solving is a major bottleneck in verification and program- analysis pipelines. Existing parallelization techniques either operate within a particular solver or partition formulas using syntactic Boolean structure from the input query. We present ThunderFork, a solver-agnostic preprocessor that combines LLVM-based simplification with selective case splitting to generate independent subqueries for parallel execution by an unmodified SMT solver. By operating on optimized LLVM IR, ThunderFork can split both input-level conditionals and conditional structure introduced during optimization. Pre- liminary evaluation of 44 satisfiable SMT-LIB benchmarks finds a 1.036× geometric-mean speedup for our cost-guided policy over SMT-LLVM Optimizing Translation (SLOT).
Article Search
Article: splashcomp26src-p14-p (type: Extended Abstract) doi:10.1145/3837729.3839577
SPLASH Companion '26: "OLIVE: Output-Level Iterative ..."
OLIVE: Output-Level Iterative Verification Engine
Aila Jahromi, Junhao Gao, Zhixuan He, and Jonathan Mendoza
(University of California at San Diego, USA)
Large language models (LLMs) can effectively generate action plans from natural-language descriptions but provide no guarantees that their outputs satisfy domain-specific safety requirements. This limitation is particularly concerning in safety-critical domains such as emergency medicine, where protocol violations can jeopardize patient safety. We present OLIVE, a framework that combines LLM-generated plans with automated repair to automatically generate medical procedures with formally verified safety guarantees. OLIVE encodes established medical safety protocols as logical constraints in the Alloy specification language and verifies candidate plans against them. When verification identifies protocol violations, OLIVE incorporates the resulting counterexample directly into the generation loop to iteratively repair the candidate plan while preserving the LLM’s context-sensitive reasoning. We evaluate OLIVE on emergency medical scenarios derived from established clinical protocols and demonstrate that it automatically repairs protocol violations to produce plans that satisfy all specified safety requirements.
Article Search
Article: splashcomp26src-p3-p (type: Extended Abstract) doi:10.1145/3837729.3839568
SPLASH Companion '26: "CoCoMUT: A Tool for Code-Context ..."
CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation
Alessandro Botta, Shiven Garisa, Jaya Vardhini Akurathi, Ahsanul Ameen Sabit, Trey Woodlief, and Soneya Binta Hossain
(University of Texas at Dallas, USA; Heritage High School, USA; William & Mary, USA)
Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-type information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects.
We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at type, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, type, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques.
The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99% of generated context records passed all applicable correctness checks.
Demo: https://youtu.be/RCUzkCQjG30 Artifact: https://github.com/assert-lab/CoCoMUT
Article Search
Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485
SPLASH Companion '26: "FlowLog: Re-thinking Datalog ..."
FlowLog: Re-thinking Datalog for Fast and Extensible Static Analysis
Zhenghong Yu, Hangdong Zhao, Wanzhu Hou, and Paraschos Koutris
(University of Wisconsin-Madison, USA; Microsoft Gray Systems Lab, USA)
Datalog is widely used to build static analyzers, yet existing engines often force a tradeoff between efficiency and extensibility. In practice, static analyses are not run once and forgotten: users edit facts, tune rules, diagnose bottlenecks, and often need semantics beyond standard Datalog, leaving these tasks to ad hoc tooling or invasive engine rewrites.
We demonstrate FlowLog, a Datalog compiler that turns Soufflé-style programs into Differential Dataflow executables for efficient and extensible static analysis. Across 24 benchmarks derived from real-world workloads, FlowLog consistently outperforms state-of-the-art engines in runtime while remaining memory-efficient and scaling better.
The demonstration uses a DOOP points-to analysis. Attendees run it, switching the same program from one-shot to incremental evaluation that retracts a fact and updates results in milliseconds; tune it, inspecting per-operator costs in a browser-based profiler and repairing a bad join order; and extend it with a k-core example beyond standard Datalog.
Article Search
Artifacts Available
Article: splashcomp26demo-p3-p (type: Short Paper) doi:10.1145/3837729.3840480
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "Bridging Call Boundaries: ..."
Bridging Call Boundaries: Inter-procedural Semantic Completion for Graph-Based Vulnerability Detection
Ruiguo Hu, Dongqi Wang, Shujin Yang, Zhenglin Li, and Dongming Chen
(Northeastern University, China)
Deep learning-based vulnerability detection approaches are limited when vulnerabilities involve multiple functions, where the security effect of a function depends on the behavior of invoked functions. As a result, function-level models may miss key vulnerability-related information across call boundaries. To address this issue, we propose VulSCG, a graph-based vulnerability detection framework with inter-procedural semantic completion. VulSCG first retrieves callee implementations from the corresponding project version and uses LLMs to generate structured summaries of their input, output and security-relevant behaviors. The generated summaries are injected into the caller Code Property Graph as SummaryNodes, allowing inter-procedural security semantics to participate in graph learning without expanding the full callee graph. Experiments on Devign show that VulSCG outperforms representative learning-based vulnerability detection baselines. In particular, VulSCG achieves the best F1 score on the dataset, with a F1 improvement of 4.25% over the strongest baseline. These results indicate that VulSCG improves detection effectiveness while maintaining scalability, since it complements inter-procedural semantics through compact SummaryNodes rather than full callee graph expansion.
Article Search
Article: splashcomp26poster-p5-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839590
SPLASH Companion '26: "OLIVE: Output-Level Iterative ..."
OLIVE: Output-Level Iterative Verification Engine
Aila Jahromi, Junhao Gao, Zhixuan He, and Jonathan Mendoza
(University of California at San Diego, USA)
Large language models (LLMs) can effectively generate action plans from natural-language descriptions but provide no guarantees that their outputs satisfy domain-specific safety requirements. This limitation is particularly concerning in safety-critical domains such as emergency medicine, where protocol violations can jeopardize patient safety. We present OLIVE, a framework that combines LLM-generated plans with automated repair to automatically generate medical procedures with formally verified safety guarantees. OLIVE encodes established medical safety protocols as logical constraints in the Alloy specification language and verifies candidate plans against them. When verification identifies protocol violations, OLIVE incorporates the resulting counterexample directly into the generation loop to iteratively repair the candidate plan while preserving the LLM’s context-sensitive reasoning. We evaluate OLIVE on emergency medical scenarios derived from established clinical protocols and demonstrate that it automatically repairs protocol violations to produce plans that satisfy all specified safety requirements.
Article Search
Article: splashcomp26src-p3-p (type: Extended Abstract) doi:10.1145/3837729.3839568
SPLASH Companion '26: "Falconf: A Web-Based Tool ..."
Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis
Youyang Kim, Sahil Suneja, Yong-Hwan Jeong, Yunja Choi, Young-Woo Kwon, and Byungchul Tak
(Kyungpook National University, Republic of Korea; IBM Research, USA)
Misconfigurations continue to be one of the major causes of failures in distributed software systems, yet diagnosing them remains challenging. This is because faulty configuration parameters are difficult to identify among hundreds of configuration entries, and their effects often leave no explicit evidence in runtime logs. We present Falconf, a web-based tool for automatically diagnosing misconfigurations in distributed software systems using log analysis. Falconf takes runtime log files as input, analyzes them using a pre-trained two-stage transformer model, and produces a ranked list of suspicious configuration parameters that are likely responsible for the observed failure. The tool features an intuitive web interface that visualizes the diagnosis workflow, allowing users to select the target application and version, input log files, and inspect the ranked results without any expertise in machine learning or log analysis. We demonstrate that Falconf can effectively diagnose misconfigured parameters from real-world logs of distributed software systems, including Apache Spark and Hadoop.
Article Search
Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499
SPLASH Companion '26: "SCOUT: A Scenario-Guided Unit ..."
SCOUT: A Scenario-Guided Unit Test Generation Tool for Compact Open-Source LLMs
Myungho Lee, Seokhyeon Moon, Yoon-Chan Jhi, and Hakjoo Oh
(Samsung SDS, Republic of Korea; Korea University, Republic of Korea)
Large language models (LLMs) have shown promising performance in automated unit test generation, but existing approaches often rely on large proprietary or reasoning-oriented models, limiting their practicality for users with limited computational resources. We present SCOUT, a scenario-guided unit test generation tool designed for compact open-source LLMs. Rather than requiring LLMs to reason over raw source code, SCOUT extracts program information through static analysis and progressively provides concise, task-specific contexts for specialized reasoning tasks, including scenario construction and unit test generation. The tool further validates and refines generated tests using compilation, execution, and coverage feedback. Built on an extensible multi-agent architecture, SCOUT provides a fully automated workflow that enables practical unit test generation with locally deployed open-source LLMs on commodity hardware.
Article Search
Article: splashcomp26demo-p44-p (type: Short Paper) doi:10.1145/3837729.3840501
SPLASH Companion '26: "PyMut4SE: Comprehensive Mutation ..."
PyMut4SE: Comprehensive Mutation Testing for Python
Laura Plein, Matthieu Jimenez, and Mike Papadakis
(CISPA Helmholtz Center for Information Security, Germany; University of Luxembourg, Luxembourg)
Mutation analysis involves examining the behavior of program mutants to identify meaningful behavioural differences, with the aim of supporting a wide range of software engineering activities, including testing, debugging, program improvement, change impact analysis, and the understanding of modified program behavior. A critical aspect of mutation analysis lies in the quality of the mutations employed, as inadequate mutation sets can lead to poor observations and, consequently, unreliable results. To address this challenge, we present PyMut4SE, a novel mutation tool for Python that focuses on a comprehensive set of mutations for any Python project. PyMut4SE stores mutants, along with their associated metadata and behavioral outcomes, in an SQLite database, allowing for a variety of downstream software engineering tasks. The tool is designed to support fundamental research in software engineering by providing a rich and extensible set of mutation operators, access to mutated source code and its characteristics, detailed execution and behavioral observations, and support for both selective mutation and the generation of higher-order mutants.
Article Search
Article: splashcomp26demo-p34-p (type: Short Paper) doi:10.1145/3837729.3840494
SPLASH Companion '26: "ADEPT: A Unified Framework ..."
ADEPT: A Unified Framework for Deep Learning Test Adequacy
Yidi Kao, Shawn Burnham, Tommi Rose Fahy, and Ali Ghanbari
(Auburn University, USA)
Over the past decade, many test adequacy metrics have been proposed for deep learning that characterize test dataset adequacy from different perspectives, e.g., neuron activation behavior, latent feature coverage, decision-boundary exploration, etc. However, these metrics are typically released as independent research prototypes with substantially different installation and preprocessing requirements, execution workflows, and configuration mechanisms. These complications make them quite difficult to reproduce, compare, and adopt in research work and practical deployment alike. In this paper, we present the engineering details of ADEPT, a framework that integrates representative adequacy techniques, including neuron-coverage-based metrics, surprise adequacy, input distribution coverage, boundary coverage, and source- and model-level mutation score, under a consistent execution workflow. ADEPT provides a template-based metric interface with well-defined extension points for integrating new adequacy metrics. Furthermore, it provides YAML-based configuration management, preprocessing-cache reuse, and structured result reporting, making it easy to use in any research and development workflows. ADEPT is designed for researchers and practitioners who wish to reproduce and apply adequacy metrics without spending days or weeks implementing missing tooling or configuring disparate research prototypes. A demo video is available at https://aub.ie/ADEPT_video.
Article Search
Article: splashcomp26demo-p14-p (type: Short Paper) doi:10.1145/3837729.3840488
SPLASH Companion '26: "Query Analyzer: Framework-Agnostic, ..."
Query Analyzer: Framework-Agnostic, Confidence-Based N+1 Detection for the JVM
Mahmoud Khawaja
(Cairo University, Egypt)
The N+1 query problem (issuing one database query per element of a collection instead of a single batched query) is among the most common and costly performance defects in data-access code, yet tool support on the Java Virtual Machine (JVM) is fragmented. Raw Java Database Connectivity (JDBC) interceptors log statements but do not detect anti-patterns; test-time assertion libraries detect N+1 only inside unit tests, are typically tied to Hibernate, and flag any repeated query, producing false positives on legitimate patterns such as pagination and polling. We present Query Analyzer, an open-source tool that automatically detects N+1 queries, analyzes their query plans, and suggests fixes. It intercepts queries at the JDBC layer, so it works across frameworks (Hibernate, Spring Data JPA, MyBatis, jOOQ, plain JDBC); it runs both as a @NoNPlusOne JUnit 5 regression guard and as a production servlet filter with per-endpoint reporting; and it uses a confidence model with explicit false-positive suppression to separate true N+1s from legitimate repetition. It additionally analyzes EXPLAIN plans and emits framework-specific fix suggestions. Dropped into unmodified real-world applications—Spring PetClinic and a third-party many-to-many sample—Query Analyzer detects real N+1s at high confidence, each pinpointed to a stack frame, and its own suggested fix eliminates them. On a controlled benchmark it cleanly separates true N+1s from legitimate repetition (pagination, polling, batched reads) where a count-based rule and the live JPlusOne detector cannot (F1 1.00 versus 0.57 and 0.67 on the suite). Query Analyzer is on Maven Central and ships a one-command reproduction package.
Article Search
Artifacts Available
Article: splashcomp26demo-p8-p (type: Short Paper) doi:10.1145/3837729.3840484
SPLASH Companion '26: "VarCHEKER: A Variability-Based ..."
VarCHEKER: A Variability-Based Static Analyzer for Python Applications
Chin Khor, Robyn Lutz, and Amir Niaraki
(Iowa State University, USA; Musco Sports Lighting, USA)
Variability-aware analysis plays an important role in early defect detection by identifying inconsistencies between variability requirements and their implementation in code. Such analysis is especially needed when developing configurable software and product lines. While many variability-aware parsers have been developed for C/C++ program analysis, support for Python programs remains limited. This paper presents VarCHEKER, a new, open-source tool for variability requirements-based analysis of Python programs. Results from its evaluation on an industrial Python application found it effective in detecting inconsistencies between the variability requirements and the implemented code.
Article Search
Article: splashcomp26demo-p11-p (type: Short Paper) doi:10.1145/3837729.3840487
SPLASH Companion '26: "Falconf: A Web-Based Tool ..."
Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis
Youyang Kim, Sahil Suneja, Yong-Hwan Jeong, Yunja Choi, Young-Woo Kwon, and Byungchul Tak
(Kyungpook National University, Republic of Korea; IBM Research, USA)
Misconfigurations continue to be one of the major causes of failures in distributed software systems, yet diagnosing them remains challenging. This is because faulty configuration parameters are difficult to identify among hundreds of configuration entries, and their effects often leave no explicit evidence in runtime logs. We present Falconf, a web-based tool for automatically diagnosing misconfigurations in distributed software systems using log analysis. Falconf takes runtime log files as input, analyzes them using a pre-trained two-stage transformer model, and produces a ranked list of suspicious configuration parameters that are likely responsible for the observed failure. The tool features an intuitive web interface that visualizes the diagnosis workflow, allowing users to select the target application and version, input log files, and inspect the ranked results without any expertise in machine learning or log analysis. We demonstrate that Falconf can effectively diagnose misconfigured parameters from real-world logs of distributed software systems, including Apache Spark and Hadoop.
Article Search
Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499
SPLASH Companion '26: "RepairFormer: Automated Repair ..."
RepairFormer: Automated Repair of Structured Inputs using Transformers
Ovi Paul, Tom J. King, and Ali Shokri
(University of Houston, USA)
Structured input files such as JSON, S-expression, DOT, OBJ, INI, and TinyC are widely used in software systems, but small corruptions can cause parsers to reject otherwise useful data. Repairing such inputs is important because malformed configuration, program, and data files can interrupt testing, analysis, deployment, and downstream automation even when most of the original content remains intact. Existing repair techniques can produce structurally valid inputs, but they often rely on deletion or repeated search, which may lose original content and result in semantic incorrectness. This paper presents RepairFormer, a transformer-based framework for structured input repair. The approach formulates repair as a supervised sequence generation task and uses format tags, oracle validation, and boundary-localized repair to generate valid outputs while preserving content. The boundary workflow focuses generation on the detected fault region, reducing the input size, and supporting repair of longer files. In evaluation, RepairFormer achieves a 88% in repair and 94% in recovery, showing strongest content preservation when repairs are successful. Additional experiments on our benchmark shows RepairFormer repairs 97.57% and recovers 94.29% with 5x faster runtime compared to state of the art.
Article Search
Artifacts Available
Article: splashcomp26demo-p37-p (type: Short Paper) doi:10.1145/3837729.3840497
SPLASH Companion '26: "Fusion: A Fold and Unfold ..."
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
Joonghoon Lee, Nicolas Klose, Seokhyun Lee, Peter Müller, and Hakjoo Oh
(Korea University, Republic of Korea; ETH Zurich, Switzerland)
Viper is a verification infrastructure for permission-based reasoning and serves as a common back-end for verifiers targeting multiple programming languages. In Viper, predicates package heap resources into reusable abstractions. To prevent SMT solvers from unfolding recursive predicates indefinitely, Viper treats predicates isorecursively: a predicate instance is not automatically interchangeable with the resources described by its body. Consequently, users must provide explicit fold/unfold annotations to transition between abstraction levels.
To address this issue, we present Fusion, a Viper-based tool that synthesizes missing fold/unfold annotations, built around a novel graph-based synthesis method. Given a verification failure due to a missing resource, Fusion constructs a predicate dependency graph from Viper predicate definitions and finds potential ways to obtain the missing resource from available resources, thereby formulating annotation synthesis as a pathfinding problem over the graph. It uses the resulting paths to synthesize candidate sequences of fold/unfold annotations that potentially provide the missing resource, and uses the verifier to validate the annotations. Our evaluation on a large real-world verification project shows that Fusion successfully synthesizes annotations for 93 of 149 benchmark functions (62.4%) within a 20-minute per-function budget, demonstrating its potential to reduce the annotation burden in practical verification workflows.
Article Search
Article: splashcomp26demo-p4-p (type: Short Paper) doi:10.1145/3837729.3840481
SPLASH Companion '26: "FlowLog: Re-thinking Datalog ..."
FlowLog: Re-thinking Datalog for Fast and Extensible Static Analysis
Zhenghong Yu, Hangdong Zhao, Wanzhu Hou, and Paraschos Koutris
(University of Wisconsin-Madison, USA; Microsoft Gray Systems Lab, USA)
Datalog is widely used to build static analyzers, yet existing engines often force a tradeoff between efficiency and extensibility. In practice, static analyses are not run once and forgotten: users edit facts, tune rules, diagnose bottlenecks, and often need semantics beyond standard Datalog, leaving these tasks to ad hoc tooling or invasive engine rewrites.
We demonstrate FlowLog, a Datalog compiler that turns Soufflé-style programs into Differential Dataflow executables for efficient and extensible static analysis. Across 24 benchmarks derived from real-world workloads, FlowLog consistently outperforms state-of-the-art engines in runtime while remaining memory-efficient and scaling better.
The demonstration uses a DOOP points-to analysis. Attendees run it, switching the same program from one-shot to incremental evaluation that retracts a fact and updates results in milliseconds; tune it, inspecting per-operator costs in a browser-based profiler and repairing a bad join order; and extend it with a k-core example beyond standard Datalog.
Article Search
Artifacts Available
Article: splashcomp26demo-p3-p (type: Short Paper) doi:10.1145/3837729.3840480
SPLASH Companion '26: "bench: A Programmable Command-Line ..."
bench: A Programmable Command-Line Framework for Complex Benchmarking Workflows
Filip Říha and Filip Křikava
(Czech Technical University, Czech Republic)
Benchmarking provides much of the feedback that drives systems and language research, yet sound benchmarking is hard. As experiments grow, added programs, configurations, custom metrics, warmup, failures, and machine noise can all mislead. We present bench, a tool that keeps simple measurements simple and lets complex experiments scale without leaving a general-purpose language. It offers a command-line interface for ad-hoc runs and a small, almost declarative Python API for repeatable experiments, both backed by one engine. A builder API resolves a suite of benchmarks lazily against a typed context, so a single script can be parametrized from the command line, discover its workloads at run time, and treat process benchmarks and in-process harnesses through one pipeline. We have used it to simplify the benchmarking infrastructure for our R just-in-time compilers, to evaluate student language implementations in a course, and to drive established suites such as Renaissance and SPEC.
Article Search
Article: splashcomp26demo-p46-p (type: Short Paper) doi:10.1145/3837729.3840502
SPLASH Companion '26: "Falconf: A Web-Based Tool ..."
Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis
Youyang Kim, Sahil Suneja, Yong-Hwan Jeong, Yunja Choi, Young-Woo Kwon, and Byungchul Tak
(Kyungpook National University, Republic of Korea; IBM Research, USA)
Misconfigurations continue to be one of the major causes of failures in distributed software systems, yet diagnosing them remains challenging. This is because faulty configuration parameters are difficult to identify among hundreds of configuration entries, and their effects often leave no explicit evidence in runtime logs. We present Falconf, a web-based tool for automatically diagnosing misconfigurations in distributed software systems using log analysis. Falconf takes runtime log files as input, analyzes them using a pre-trained two-stage transformer model, and produces a ranked list of suspicious configuration parameters that are likely responsible for the observed failure. The tool features an intuitive web interface that visualizes the diagnosis workflow, allowing users to select the target application and version, input log files, and inspect the ranked results without any expertise in machine learning or log analysis. We demonstrate that Falconf can effectively diagnose misconfigured parameters from real-world logs of distributed software systems, including Apache Spark and Hadoop.
Article Search
Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499
SPLASH Companion '26: "Iekkë: A Bounded-Round Partial-Order ..."
Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, and Gennaro Parlato
(Gran Sasso Science Institute, Italy; Stellenbosch University, South Africa; University of Salerno, Italy; Diffblue, UK; University of Molise, Italy)
We present Iekkë, a BMC tool for verifying multi-threaded C programs. It implements a new bounded-round partial-order encoding for the sequential consistency shared-memory model. The encoding combinesbthe compactness of lazy sequentialization with the structural precision of the partial-order approach. Its concurrency constraints grow linearly in the number of shared-memory events and in the round bound 𝑘—--avoiding the quadratic/cubic blow-up of classical partial-order encodings—--and are fully propositional, enabling the use of an off-the-shelf SAT solver. Iekkë is built on top of the CBMC/Deagle infrastructure and replaces only the concurrency constraint module. It supports concurrent reachability checking, data race detection, and the usual safety property checks implemented by CBMC. Iekkë won the Bronze medal in the Concurrency category of SV-COMP 2026.
Article Search
Article: splashcomp26demo-p18-p (type: Short Paper) doi:10.1145/3837729.3840491
SPLASH Companion '26: "Do Machines Struggle Where ..."
Do Machines Struggle Where Humans Do? Obfuscation as a Probe of Human and Machine Code Comprehension
Jack Le
(University of Texas at Dallas, USA)
Code obfuscation targets human comprehension, but current evaluations primarily measure language model performance degradation instead of whether models fail in the same way as humans. A direct comparison across five obfuscation tiers reveals that comprehension difficulty is non-monotonic. Only reasoning-tuned models mirror human difficulty patterns. This alignment, rather than raw accuracy, distinguishes robust comprehension from brittle pattern matching.
Article Search
Article: splashcomp26src-p10-p (type: Extended Abstract) doi:10.1145/3837729.3839573
SPLASH Companion '26: "Fusion: A Fold and Unfold ..."
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
Joonghoon Lee, Nicolas Klose, Seokhyun Lee, Peter Müller, and Hakjoo Oh
(Korea University, Republic of Korea; ETH Zurich, Switzerland)
Viper is a verification infrastructure for permission-based reasoning and serves as a common back-end for verifiers targeting multiple programming languages. In Viper, predicates package heap resources into reusable abstractions. To prevent SMT solvers from unfolding recursive predicates indefinitely, Viper treats predicates isorecursively: a predicate instance is not automatically interchangeable with the resources described by its body. Consequently, users must provide explicit fold/unfold annotations to transition between abstraction levels.
To address this issue, we present Fusion, a Viper-based tool that synthesizes missing fold/unfold annotations, built around a novel graph-based synthesis method. Given a verification failure due to a missing resource, Fusion constructs a predicate dependency graph from Viper predicate definitions and finds potential ways to obtain the missing resource from available resources, thereby formulating annotation synthesis as a pathfinding problem over the graph. It uses the resulting paths to synthesize candidate sequences of fold/unfold annotations that potentially provide the missing resource, and uses the verifier to validate the annotations. Our evaluation on a large real-world verification project shows that Fusion successfully synthesizes annotations for 93 of 149 benchmark functions (62.4%) within a 20-minute per-function budget, demonstrating its potential to reduce the annotation burden in practical verification workflows.
Article Search
Article: splashcomp26demo-p4-p (type: Short Paper) doi:10.1145/3837729.3840481
SPLASH Companion '26: "SCOUT: A Scenario-Guided Unit ..."
SCOUT: A Scenario-Guided Unit Test Generation Tool for Compact Open-Source LLMs
Myungho Lee, Seokhyeon Moon, Yoon-Chan Jhi, and Hakjoo Oh
(Samsung SDS, Republic of Korea; Korea University, Republic of Korea)
Large language models (LLMs) have shown promising performance in automated unit test generation, but existing approaches often rely on large proprietary or reasoning-oriented models, limiting their practicality for users with limited computational resources. We present SCOUT, a scenario-guided unit test generation tool designed for compact open-source LLMs. Rather than requiring LLMs to reason over raw source code, SCOUT extracts program information through static analysis and progressively provides concise, task-specific contexts for specialized reasoning tasks, including scenario construction and unit test generation. The tool further validates and refines generated tests using compilation, execution, and coverage feedback. Built on an extensible multi-agent architecture, SCOUT provides a fully automated workflow that enables practical unit test generation with locally deployed open-source LLMs on commodity hardware.
Article Search
Article: splashcomp26demo-p44-p (type: Short Paper) doi:10.1145/3837729.3840501
SPLASH Companion '26: "Fusion: A Fold and Unfold ..."
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
Joonghoon Lee, Nicolas Klose, Seokhyun Lee, Peter Müller, and Hakjoo Oh
(Korea University, Republic of Korea; ETH Zurich, Switzerland)
Viper is a verification infrastructure for permission-based reasoning and serves as a common back-end for verifiers targeting multiple programming languages. In Viper, predicates package heap resources into reusable abstractions. To prevent SMT solvers from unfolding recursive predicates indefinitely, Viper treats predicates isorecursively: a predicate instance is not automatically interchangeable with the resources described by its body. Consequently, users must provide explicit fold/unfold annotations to transition between abstraction levels.
To address this issue, we present Fusion, a Viper-based tool that synthesizes missing fold/unfold annotations, built around a novel graph-based synthesis method. Given a verification failure due to a missing resource, Fusion constructs a predicate dependency graph from Viper predicate definitions and finds potential ways to obtain the missing resource from available resources, thereby formulating annotation synthesis as a pathfinding problem over the graph. It uses the resulting paths to synthesize candidate sequences of fold/unfold annotations that potentially provide the missing resource, and uses the verifier to validate the annotations. Our evaluation on a large real-world verification project shows that Fusion successfully synthesizes annotations for 93 of 149 benchmark functions (62.4%) within a 20-minute per-function budget, demonstrating its potential to reduce the annotation burden in practical verification workflows.
Article Search
Article: splashcomp26demo-p4-p (type: Short Paper) doi:10.1145/3837729.3840481
SPLASH Companion '26: "Dredd: Scalable Source-Level ..."
Dredd: Scalable Source-Level Mutation Testing for Large C/C++ Codebases
Alastair F. Donaldson, James Lee-Jones, and Jonathan Foo
(Imperial College London, UK)
We present Dredd, a new tool that supports source-level mutation testing for large C/C++ codebases. Following the mutant schemata approach, Dredd applies a source-to-source transformation to a chosen set of files from the system under test (SUT), rewriting them into a metamutant that simulates a large number of distinct mutants, each selected via an environment variable holding the desired mutant’s ID. With no mutant selected, the metamutant behaves like the original SUT; otherwise it behaves as if a specific edit—such as replacing a binary operator or deleting a statement—had been applied. Because the metamutant is compiled and linked only once, mutation analysis across many mutants avoids expensive per-mutant recompilation and linking. We evaluate Dredd’s scalability on the Clang/LLVM compiler (a large C++ project) and the zstd compression library (a sizeable C project), and showcase an application of Dredd in compiler testing, using it to compare how effective the Csmith and YARPGen v1 and v2 tools are at killing mutants in Clang/LLVM.
Article Search
Article: splashcomp26demo-p6-p (type: Short Paper) doi:10.1145/3837729.3840482
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "After the Hitchhiker’s Guide: ..."
After the Hitchhiker’s Guide: Toward Principled LLM Assistance for Static Analysis
Haonan Li
(University of California at Riverside, USA)
Practical static analysis of large systems such as the Linux kernel often depends on information that is difficult to capture precisely and on identifying the parts of a large codebase where precise reasoning is needed. This dissertation studies how LLMs can complement static analysis through two roles: specification recovery and analysis localization. The first part shows that LLMs can refine static-analysis warnings when guided by program-analysis principles; in LLift (OOPSLA’24) and BugLens (ASE’25), these workflows reduce false positives and uncover genuine Linux kernel bugs. Building on these results, the next part moves more of the program reasoning back into the analyzer, while using LLMs to recover specifications and localize analysis targets. Their outputs then become explicit premises for analysis rather than final bug judgments. The remaining work studies how these premises can be validated or qualified before they affect analysis results.
Article Search
Article: splashcomp26doc-p18-p (type: Extended Abstract) doi:10.1145/3837729.3842145
SPLASH Companion '26: "Bridging Call Boundaries: ..."
Bridging Call Boundaries: Inter-procedural Semantic Completion for Graph-Based Vulnerability Detection
Ruiguo Hu, Dongqi Wang, Shujin Yang, Zhenglin Li, and Dongming Chen
(Northeastern University, China)
Deep learning-based vulnerability detection approaches are limited when vulnerabilities involve multiple functions, where the security effect of a function depends on the behavior of invoked functions. As a result, function-level models may miss key vulnerability-related information across call boundaries. To address this issue, we propose VulSCG, a graph-based vulnerability detection framework with inter-procedural semantic completion. VulSCG first retrieves callee implementations from the corresponding project version and uses LLMs to generate structured summaries of their input, output and security-relevant behaviors. The generated summaries are injected into the caller Code Property Graph as SummaryNodes, allowing inter-procedural security semantics to participate in graph learning without expanding the full callee graph. Experiments on Devign show that VulSCG outperforms representative learning-based vulnerability detection baselines. In particular, VulSCG achieves the best F1 score on the dataset, with a F1 improvement of 4.25% over the strongest baseline. These results indicate that VulSCG improves detection effectiveness while maintaining scalability, since it complements inter-procedural semantics through compact SummaryNodes rather than full callee graph expansion.
Article Search
Article: splashcomp26poster-p5-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839590
SPLASH Companion '26: "CrossLangFuzzer: Differential ..."
CrossLangFuzzer: Differential Testing of Cross-Language JVM Compilers
Xiaotian Ma, Qiong Feng, Yongqiang Tian, Wei Song, and Peng Liang
(Nanjing University of Science and Technology, China; Monash University, Australia; Wuhan University, China)
Modern JVM software increasingly integrates multiple programming languages, such as Java, Kotlin, Groovy, and Scala, within a single application. Supporting such interoperability requires JVM compilers to perform cross-language compilation while reconciling subtle semantic differences across language boundaries. Errors in this process can lead to critical miscompilations, yet existing compiler testing techniques focus exclusively on isolated, single-language compilation. To address this gap, we present CrossLangFuzzer, the first differential testing framework for cross-language JVM compilation. CrossLangFuzzer leverages the Kotlin compiler's unified intermediate representation (IR) to synthesize cross language test programs. It further applies seven mutation operators to diversify generated test programs and improve bug-finding capability. Evaluated on the latest versions of five major JVM compilers, CrossLangFuzzer uncovered 32 confirmed bugs, including 15 in Kotlin, 4 in Groovy, 7 in Scala 3, 2 in Scala 2, and 4 in Java.
Article Search
Article: splashcomp26demo-p21-p (type: Short Paper) doi:10.1145/3837729.3840493
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "RepoTrace: Browser-Assisted ..."
RepoTrace: Browser-Assisted Evidence Collection for GitHub Research Datasets
Xue Yao, Zehua Zhang, Jiatong Liu, and Yongqiang Tian
(Monash University, Australia)
Empirical software engineering studies frequently build datasets from GitHub issues and pull requests. In many projects, researchers inspect pages in a browser, copy selected fields into spreadsheets, keep side notes in separate documents, and later run scripts to normalize or export the data. This workflow is flexible, but the page evidence, the research codes, and the rationale behind each decision end up spread across tabs and files, making provenance, update tracking, and multi-reviewer labeling difficult to audit.
RepoTrace is a browser-assisted research tool that collects GitHub issue and pull-request evidence into a local SQLite-backed workspace. It combines a Chrome side-panel extension, an Express backend, and a React dashboard to capture page snapshots, comments, labels, notes, screening and labeling decisions, refresh history, and scoped exports, keeping the source evidence and the research interpretation linked together.
A validation pass covered 20 Matplotlib issues across two study projects. The resulting dataset preserves 22 snapshots, 38 comments, 20 research notes, 98 annotations, 20 screening reviews, 20 fix-evidence entries, and 4 simulated unresolved consensus conflicts. The results show that RepoTrace can support a complete local evidence-collection workflow for manually constructed GitHub issue and pull-request datasets.
Article Search
Article: splashcomp26demo-p39-p (type: Short Paper) doi:10.1145/3837729.3840498
SPLASH Companion '26: "DebugTracker: Lightweight ..."
DebugTracker: Lightweight Process Evidence for Classroom Debugging
Jiatong Liu, Xue Yao, Zehua Zhang, and Yongqiang Tian
(Monash University, Australia)
Debugging exercises are often assessed from final code and test outcomes, yet these artifacts hide how students reproduced failures, formed hypotheses, inspected evidence, edited code, and verified fixes. We present DebugTracker, a Visual Studio Code extension that records lightweight debugging-process evidence for classroom tasks. DebugTracker separates uncoached Evaluation Mode traces from coached Training Mode traces, stores append-only JSONL events, and exports timeline and Markdown reports for human review. The prototype records test commands, editor and debugger metadata, student checkpoints, source snapshots, and human labels. It can also record optional image evidence and AI-assisted practice feedback. DebugTracker is largely language-agnostic: it captures process evidence through standard VS Code mechanisms rather than language-specific tooling, although debugger evidence depends on the relevant VS Code language extension. We validate the prototype with debugging tasks in Python, TypeScript, and Java, 16 automated checks, and an 11-case manual trial matrix spanning packaged VSIX installation and three operating systems.
Article Search
Article: splashcomp26demo-p43-p (type: Short Paper) doi:10.1145/3837729.3840500
SPLASH Companion '26: "LPR+: Diverse Transformations ..."
LPR+: Diverse Transformations for LLM-Aided Program Reduction
Zehua Zhang, Jiatong Liu, Xue Yao, and Yongqiang Tian
(Monash University, Australia)
Program reduction helps compiler and language-tool developers turn large failure-inducing programs into small, shareable bug reports. LPR (Large Language Models-Aided Program Reduction) demonstrated that large language models (LLMs) can complement syntax-guided reducers by proposing language-specific transformations once a generic reducer has made the input small enough for a model. However, LPR's prompt catalog contains only five broad transformation categories, leaving much of the space explored by conventional reducers implicit. We present LPR+, which makes this transformation space explicit. LPR+ keeps LPR's oracle-validated discipline, in which every candidate must still be smaller and preserve the interesting behavior, and adds thirty refined, reducer-inspired rules derived from observations of C-Reduce, Perses, and Vulcan and provided as prompts rather than trusted rewrites. On the LPR benchmark across C, Rust, and JavaScript with gpt-5.4-mini, LPR+ lowers the mean final size from 189.7 to 180.9 tokens on the cases completed by both protocols, at the cost of additional model queries. These results suggest that an explicit, oracle-validated transformation catalog provides an extension point for LLM-aided program reduction. The demonstration video is available at https://youtu.be/kNULghJH-2E.
Article Search
Article: splashcomp26demo-p48-p (type: Short Paper) doi:10.1145/3837729.3840504
SPLASH Companion '26: "Detecting Silent Java GC Bugs ..."
Detecting Silent Java GC Bugs via Anomalous Runtime Behavior
Ye Liu
(Nanjing University, China)
Java garbage collectors (GCs) are critical for JVM, yet they can exhibit silent efficiency bugs: programs produce correct results but trigger excessive full GCs, long stop-the-world pauses, or ineffective heap expansion.Existing JVM and GC testing relies largely on crashes, output mismatches, or coverage feedback, leaving such bugs undetected.We present GCDiff, a differential testing method that executes test programs across a matrix of JDK versions and GCs, extracts GC event counts, STW pauses, and committed-heap capacity from GC logs, and applies a three-channel anomaly detection model to rank suspicious execution configurations. Applied to OpenJDK, GCDiff discovered 8 bugs; 6 were confirmed, including 3 that were fixed. One was a JDK 26 ParallelGC heap-expansion bug that triggered thousands of Full GCs.
Article Search
Article: splashcomp26src-p20-p (type: Extended Abstract) doi:10.1145/3837729.3839582
SPLASH Companion '26: "OpenRepair: An Automated Tool ..."
OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs
Jinning Zhang, Bin Yu, Haoli Zhang, Letian Wang, Wensheng Wang, and Xu Lu
(Xidian University, China)
OpenMP is a widely adopted shared-memory programming model, yet its concurrent execution is highly prone to data races, threatening software correctness and performance. Existing automated repair techniques depend heavily on manually designed synchronization strategies, which limit their applicability to diverse OpenMP programs. This paper demonstrates OpenRepair, an end-to-end automated tool designed to generate context-aware data-race fixes for OpenMP applications. OpenRepair features a robust pipeline that synergizes static analysis, retrieval-augmented generation (RAG), and large language models (LLMs). By automatically digesting runtime race reports, extracting program concurrency structures, and retrieving relevant repair knowledge, the tool seamlessly synthesizes precise, template-free patches.Evaluation on 97 OpenMP benchmarks and real-world applications highlights its scalability and practical effectiveness: OpenRepair successfully resolves 85 race conditions, improving repair capability by 44.1% over existing tools while introducing lower synchronization overhead.
Article Search
Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489
SPLASH Companion '26: "VarCHEKER: A Variability-Based ..."
VarCHEKER: A Variability-Based Static Analyzer for Python Applications
Chin Khor, Robyn Lutz, and Amir Niaraki
(Iowa State University, USA; Musco Sports Lighting, USA)
Variability-aware analysis plays an important role in early defect detection by identifying inconsistencies between variability requirements and their implementation in code. Such analysis is especially needed when developing configurable software and product lines. While many variability-aware parsers have been developed for C/C++ program analysis, support for Python programs remains limited. This paper presents VarCHEKER, a new, open-source tool for variability requirements-based analysis of Python programs. Results from its evaluation on an industrial Python application found it effective in detecting inconsistencies between the variability requirements and the implemented code.
Article Search
Article: splashcomp26demo-p11-p (type: Short Paper) doi:10.1145/3837729.3840487
SPLASH Companion '26: "CrossLangFuzzer: Differential ..."
CrossLangFuzzer: Differential Testing of Cross-Language JVM Compilers
Xiaotian Ma, Qiong Feng, Yongqiang Tian, Wei Song, and Peng Liang
(Nanjing University of Science and Technology, China; Monash University, Australia; Wuhan University, China)
Modern JVM software increasingly integrates multiple programming languages, such as Java, Kotlin, Groovy, and Scala, within a single application. Supporting such interoperability requires JVM compilers to perform cross-language compilation while reconciling subtle semantic differences across language boundaries. Errors in this process can lead to critical miscompilations, yet existing compiler testing techniques focus exclusively on isolated, single-language compilation. To address this gap, we present CrossLangFuzzer, the first differential testing framework for cross-language JVM compilation. CrossLangFuzzer leverages the Kotlin compiler's unified intermediate representation (IR) to synthesize cross language test programs. It further applies seven mutation operators to diversify generated test programs and improve bug-finding capability. Evaluated on the latest versions of five major JVM compilers, CrossLangFuzzer uncovered 32 confirmed bugs, including 15 in Kotlin, 4 in Groovy, 7 in Scala 3, 2 in Scala 2, and 4 in Java.
Article Search
Article: splashcomp26demo-p21-p (type: Short Paper) doi:10.1145/3837729.3840493
SPLASH Companion '26: "Typed Template Fuzzing ..."
Typed Template Fuzzing
Lu Maltsis
(University of Manchester, UK)
Fuzzing finds bugs by testing software behavior with high volumes of input. To create semantically valid inputs for different targets, traditional fuzzers require significant engineering effort. LLM-based fuzzing approaches can be adapted to create inputs for a wide range of software but introduce new issues: every test needs an LLM query, sacrificing the speed of traditional fuzzing. We introduce Typed Template Fuzzing (TTF). It uses LLMs in a preprocessing step to create templates which encode semantic information of seed files. These templates enable semantically-aware mutations without the need for a parser, type-checker, or further LLM queries. We have implemented TTF in our tool Typos. Using Typos we have run a five-month fuzzing campaign, finding 97 previously undiscovered bugs. Typos achieves a 94.7% rate of valid inputs across a wide range of formats including SMT-LIB2, C, C++, Go, Rust, SystemVerilog, Scala, Java, and domain-specific libraries such as PyTorch and Qiskit.
Article Search
Article: splashcomp26src-p11-p (type: Extended Abstract) doi:10.1145/3837729.3839574
SPLASH Companion '26: "OLIVE: Output-Level Iterative ..."
OLIVE: Output-Level Iterative Verification Engine
Aila Jahromi, Junhao Gao, Zhixuan He, and Jonathan Mendoza
(University of California at San Diego, USA)
Large language models (LLMs) can effectively generate action plans from natural-language descriptions but provide no guarantees that their outputs satisfy domain-specific safety requirements. This limitation is particularly concerning in safety-critical domains such as emergency medicine, where protocol violations can jeopardize patient safety. We present OLIVE, a framework that combines LLM-generated plans with automated repair to automatically generate medical procedures with formally verified safety guarantees. OLIVE encodes established medical safety protocols as logical constraints in the Alloy specification language and verifies candidate plans against them. When verification identifies protocol violations, OLIVE incorporates the resulting counterexample directly into the generation loop to iteratively repair the candidate plan while preserving the LLM’s context-sensitive reasoning. We evaluate OLIVE on emergency medical scenarios derived from established clinical protocols and demonstrate that it automatically repairs protocol violations to produce plans that satisfy all specified safety requirements.
Article Search
Article: splashcomp26src-p3-p (type: Extended Abstract) doi:10.1145/3837729.3839568
SPLASH Companion '26: "A First Look at Bugs in Tile-Based ..."
A First Look at Bugs in Tile-Based GPU Programming Frameworks
Aaryaa Moharir
(University of Texas at Dallas, USA)
Tile-based programming frameworks enable deep learning and scientific computing workloads to run efficiently at scale. But their multi-stage compilation pipelines result in code generation bugs that are tightly coupled to input shapes, data types, and backend targets, and that often fail silently. These bugs are hard to catch and fix without deep knowledge of the underlying tile abstractions. Despite how widely these frameworks are deployed, the bugs they produce have received almost no systematic attention so we address that gap. Starting from 401 GitHub bug reports, we identify 301 confirmed tile-program codegen bugs and study them across five dimensions: root cause, observable symptom, triggering input, test oracle, and fix strategy. We propose the first structured characterization of this bug class, along with a foundation for building tools that are actually designed for tile-based compilers.
Article Search
Article: splashcomp26src-p18-p (type: Extended Abstract) doi:10.1145/3837729.3839580
SPLASH Companion '26: "WGSLsmith: Randomised Testing ..."
WGSLsmith: Randomised Testing for the WebGPU Shading Language
Michał Andryskowski, Amber Gorzynski, Hasan Mohsin, and Alastair F. Donaldson
(Imperial College London, UK)
We present WGSLsmith, a tool for randomised testing of compilers for the WebGPU Shading Language (WGSL). Under the WebGPU API---now supported by all three major browsers---GPU programs are written in the WebGPU Shading Language (WGSL), and every implementation ships a WGSL compiler that validates shaders and translates them to platform-specific code. Because shaders may come from untrusted websites, these compilers can be exercised by arbitrary web pages, making them a security-critical target for testing. WGSLsmith generates random shaders to find compiler crashes and cross-implementation mismatches. We describe its architecture and usage, and how we have broadened its language feature coverage to keep up to date with the evolving WGSL specification and support features absent from the original design. We report on a campaign that uncovered 12 bugs (all confirmed, 8 fixed) in various parts of the WebGPU stack, and evaluate the thoroughness of WGSLsmith via coverage analysis.
Article Search
Article: splashcomp26demo-p10-p (type: Short Paper) doi:10.1145/3837729.3840486
SPLASH Companion '26: "SCOUT: A Scenario-Guided Unit ..."
SCOUT: A Scenario-Guided Unit Test Generation Tool for Compact Open-Source LLMs
Myungho Lee, Seokhyeon Moon, Yoon-Chan Jhi, and Hakjoo Oh
(Samsung SDS, Republic of Korea; Korea University, Republic of Korea)
Large language models (LLMs) have shown promising performance in automated unit test generation, but existing approaches often rely on large proprietary or reasoning-oriented models, limiting their practicality for users with limited computational resources. We present SCOUT, a scenario-guided unit test generation tool designed for compact open-source LLMs. Rather than requiring LLMs to reason over raw source code, SCOUT extracts program information through static analysis and progressively provides concise, task-specific contexts for specialized reasoning tasks, including scenario construction and unit test generation. The tool further validates and refines generated tests using compilation, execution, and coverage feedback. Built on an extensible multi-agent architecture, SCOUT provides a fully automated workflow that enables practical unit test generation with locally deployed open-source LLMs on commodity hardware.
Article Search
Article: splashcomp26demo-p44-p (type: Short Paper) doi:10.1145/3837729.3840501
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Fusion: A Fold and Unfold ..."
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
Joonghoon Lee, Nicolas Klose, Seokhyun Lee, Peter Müller, and Hakjoo Oh
(Korea University, Republic of Korea; ETH Zurich, Switzerland)
Viper is a verification infrastructure for permission-based reasoning and serves as a common back-end for verifiers targeting multiple programming languages. In Viper, predicates package heap resources into reusable abstractions. To prevent SMT solvers from unfolding recursive predicates indefinitely, Viper treats predicates isorecursively: a predicate instance is not automatically interchangeable with the resources described by its body. Consequently, users must provide explicit fold/unfold annotations to transition between abstraction levels.
To address this issue, we present Fusion, a Viper-based tool that synthesizes missing fold/unfold annotations, built around a novel graph-based synthesis method. Given a verification failure due to a missing resource, Fusion constructs a predicate dependency graph from Viper predicate definitions and finds potential ways to obtain the missing resource from available resources, thereby formulating annotation synthesis as a pathfinding problem over the graph. It uses the resulting paths to synthesize candidate sequences of fold/unfold annotations that potentially provide the missing resource, and uses the verifier to validate the annotations. Our evaluation on a large real-world verification project shows that Fusion successfully synthesizes annotations for 93 of 149 benchmark functions (62.4%) within a 20-minute per-function budget, demonstrating its potential to reduce the annotation burden in practical verification workflows.
Article Search
Article: splashcomp26demo-p4-p (type: Short Paper) doi:10.1145/3837729.3840481
SPLASH Companion '26: "VarCHEKER: A Variability-Based ..."
VarCHEKER: A Variability-Based Static Analyzer for Python Applications
Chin Khor, Robyn Lutz, and Amir Niaraki
(Iowa State University, USA; Musco Sports Lighting, USA)
Variability-aware analysis plays an important role in early defect detection by identifying inconsistencies between variability requirements and their implementation in code. Such analysis is especially needed when developing configurable software and product lines. While many variability-aware parsers have been developed for C/C++ program analysis, support for Python programs remains limited. This paper presents VarCHEKER, a new, open-source tool for variability requirements-based analysis of Python programs. Results from its evaluation on an industrial Python application found it effective in detecting inconsistencies between the variability requirements and the implemented code.
Article Search
Article: splashcomp26demo-p11-p (type: Short Paper) doi:10.1145/3837729.3840487
SPLASH Companion '26: "Diffpoints: Breakpoints Comparing ..."
Diffpoints: Breakpoints Comparing Values of Variables
Filip Čmilňák, Matúš Sulír, and Milan Nosáľ
(Technical University of Košice, Slovakia; ValeSoft, Slovakia)
Debugging is an integral, yet time-consuming and cognitively demanding part of software development. While common debugging tools allow for a detailed inspection of current variable values, they do not offer a clear visualization of their evolution over time. When comparing states at different execution points, they rely on the programmer’s memory or auxiliary console outputs. In this paper, we present Diffpoints, a novel debugging tool that introduces new types of breakpoints to enable the automatic capture and comparison of variable states between multiple points of program execution. Two distinct types, namely line and group diffpoints, are supported, and to match variables from different stack traces, a heuristic is used. Diffpoints are implemented as an extension for the IntelliJ IDEA development environment. We conducted a preliminary user study and plan further evaluation.
Article Search
Article: splashcomp26demo-p35-p (type: Short Paper) doi:10.1145/3837729.3840495
SPLASH Companion '26: "SCOUT: A Scenario-Guided Unit ..."
SCOUT: A Scenario-Guided Unit Test Generation Tool for Compact Open-Source LLMs
Myungho Lee, Seokhyeon Moon, Yoon-Chan Jhi, and Hakjoo Oh
(Samsung SDS, Republic of Korea; Korea University, Republic of Korea)
Large language models (LLMs) have shown promising performance in automated unit test generation, but existing approaches often rely on large proprietary or reasoning-oriented models, limiting their practicality for users with limited computational resources. We present SCOUT, a scenario-guided unit test generation tool designed for compact open-source LLMs. Rather than requiring LLMs to reason over raw source code, SCOUT extracts program information through static analysis and progressively provides concise, task-specific contexts for specialized reasoning tasks, including scenario construction and unit test generation. The tool further validates and refines generated tests using compilation, execution, and coverage feedback. Built on an extensible multi-agent architecture, SCOUT provides a fully automated workflow that enables practical unit test generation with locally deployed open-source LLMs on commodity hardware.
Article Search
Article: splashcomp26demo-p44-p (type: Short Paper) doi:10.1145/3837729.3840501
SPLASH Companion '26: "Fusion: A Fold and Unfold ..."
Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification
Joonghoon Lee, Nicolas Klose, Seokhyun Lee, Peter Müller, and Hakjoo Oh
(Korea University, Republic of Korea; ETH Zurich, Switzerland)
Viper is a verification infrastructure for permission-based reasoning and serves as a common back-end for verifiers targeting multiple programming languages. In Viper, predicates package heap resources into reusable abstractions. To prevent SMT solvers from unfolding recursive predicates indefinitely, Viper treats predicates isorecursively: a predicate instance is not automatically interchangeable with the resources described by its body. Consequently, users must provide explicit fold/unfold annotations to transition between abstraction levels.
To address this issue, we present Fusion, a Viper-based tool that synthesizes missing fold/unfold annotations, built around a novel graph-based synthesis method. Given a verification failure due to a missing resource, Fusion constructs a predicate dependency graph from Viper predicate definitions and finds potential ways to obtain the missing resource from available resources, thereby formulating annotation synthesis as a pathfinding problem over the graph. It uses the resulting paths to synthesize candidate sequences of fold/unfold annotations that potentially provide the missing resource, and uses the verifier to validate the annotations. Our evaluation on a large real-world verification project shows that Fusion successfully synthesizes annotations for 93 of 149 benchmark functions (62.4%) within a 20-minute per-function budget, demonstrating its potential to reduce the annotation burden in practical verification workflows.
Article Search
Article: splashcomp26demo-p4-p (type: Short Paper) doi:10.1145/3837729.3840481
SPLASH Companion '26: "PyMut4SE: Comprehensive Mutation ..."
PyMut4SE: Comprehensive Mutation Testing for Python
Laura Plein, Matthieu Jimenez, and Mike Papadakis
(CISPA Helmholtz Center for Information Security, Germany; University of Luxembourg, Luxembourg)
Mutation analysis involves examining the behavior of program mutants to identify meaningful behavioural differences, with the aim of supporting a wide range of software engineering activities, including testing, debugging, program improvement, change impact analysis, and the understanding of modified program behavior. A critical aspect of mutation analysis lies in the quality of the mutations employed, as inadequate mutation sets can lead to poor observations and, consequently, unreliable results. To address this challenge, we present PyMut4SE, a novel mutation tool for Python that focuses on a comprehensive set of mutations for any Python project. PyMut4SE stores mutants, along with their associated metadata and behavioral outcomes, in an SQLite database, allowing for a variety of downstream software engineering tasks. The tool is designed to support fundamental research in software engineering by providing a rich and extensible set of mutation operators, access to mutated source code and its characteristics, detailed execution and behavioral observations, and support for both selective mutation and the generation of higher-order mutants.
Article Search
Article: splashcomp26demo-p34-p (type: Short Paper) doi:10.1145/3837729.3840494
SPLASH Companion '26: "Iekkë: A Bounded-Round Partial-Order ..."
Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, and Gennaro Parlato
(Gran Sasso Science Institute, Italy; Stellenbosch University, South Africa; University of Salerno, Italy; Diffblue, UK; University of Molise, Italy)
We present Iekkë, a BMC tool for verifying multi-threaded C programs. It implements a new bounded-round partial-order encoding for the sequential consistency shared-memory model. The encoding combinesbthe compactness of lazy sequentialization with the structural precision of the partial-order approach. Its concurrency constraints grow linearly in the number of shared-memory events and in the round bound 𝑘—--avoiding the quadratic/cubic blow-up of classical partial-order encodings—--and are fully propositional, enabling the use of an off-the-shelf SAT solver. Iekkë is built on top of the CBMC/Deagle infrastructure and replaces only the concurrency constraint module. It supports concurrent reachability checking, data race detection, and the usual safety property checks implemented by CBMC. Iekkë won the Bronze medal in the Concurrency category of SV-COMP 2026.
Article Search
Article: splashcomp26demo-p18-p (type: Short Paper) doi:10.1145/3837729.3840491
SPLASH Companion '26: "RepairFormer: Automated Repair ..."
RepairFormer: Automated Repair of Structured Inputs using Transformers
Ovi Paul, Tom J. King, and Ali Shokri
(University of Houston, USA)
Structured input files such as JSON, S-expression, DOT, OBJ, INI, and TinyC are widely used in software systems, but small corruptions can cause parsers to reject otherwise useful data. Repairing such inputs is important because malformed configuration, program, and data files can interrupt testing, analysis, deployment, and downstream automation even when most of the original content remains intact. Existing repair techniques can produce structurally valid inputs, but they often rely on deletion or repeated search, which may lose original content and result in semantic incorrectness. This paper presents RepairFormer, a transformer-based framework for structured input repair. The approach formulates repair as a supervised sequence generation task and uses format tags, oracle validation, and boundary-localized repair to generate valid outputs while preserving content. The boundary workflow focuses generation on the detected fault region, reducing the input size, and supporting repair of longer files. In evaluation, RepairFormer achieves a 88% in repair and 94% in recovery, showing strongest content preservation when repairs are successful. Additional experiments on our benchmark shows RepairFormer repairs 97.57% and recovers 94.29% with 5x faster runtime compared to state of the art.
Article Search
Artifacts Available
Article: splashcomp26demo-p37-p (type: Short Paper) doi:10.1145/3837729.3840497
SPLASH Companion '26: "PyMut4SE: Comprehensive Mutation ..."
PyMut4SE: Comprehensive Mutation Testing for Python
Laura Plein, Matthieu Jimenez, and Mike Papadakis
(CISPA Helmholtz Center for Information Security, Germany; University of Luxembourg, Luxembourg)
Mutation analysis involves examining the behavior of program mutants to identify meaningful behavioural differences, with the aim of supporting a wide range of software engineering activities, including testing, debugging, program improvement, change impact analysis, and the understanding of modified program behavior. A critical aspect of mutation analysis lies in the quality of the mutations employed, as inadequate mutation sets can lead to poor observations and, consequently, unreliable results. To address this challenge, we present PyMut4SE, a novel mutation tool for Python that focuses on a comprehensive set of mutations for any Python project. PyMut4SE stores mutants, along with their associated metadata and behavioral outcomes, in an SQLite database, allowing for a variety of downstream software engineering tasks. The tool is designed to support fundamental research in software engineering by providing a rich and extensible set of mutation operators, access to mutated source code and its characteristics, detailed execution and behavioral observations, and support for both selective mutation and the generation of higher-order mutants.
Article Search
Article: splashcomp26demo-p34-p (type: Short Paper) doi:10.1145/3837729.3840494
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "SentryLine: Reviewable Capability ..."
SentryLine: Reviewable Capability Traces for CPython Plugin Hosts
Haoyi Zhang and Huaijin Ran
(Xi’an Jiaotong-Liverpool University, China; Nanyang Technological University, Singapore)
SentryLine makes CPython plugin admission explainable at the boundary. The host declares which authority a plugin may exercise; SentryLine records attempted authority classes and reports or rejects the first forbidden prefix before the instrumented effect is allowed to proceed. In the packaged evaluation, the combined monitor preserves all 28 benign workloads, blocks all 72 misuse workloads, and checks 13,888 boundary decisions with zero independent-contract disagreements and zero witnessless rejections. Audit-only monitoring blocks 38 of 72 misuse workloads, which is why the poster shows both interpreter-side and wrapper-side evidence. SentryLine is an admission-time review tool, not a universal Python sandbox.
Article Search
Article: splashcomp26poster-p11-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839591
SPLASH Companion '26: "Generating Property-Based ..."
Generating Property-Based Tests for Web Applications
Savitha Ravi
(University of California at San Diego, USA)
We present SPINACH, a system that infers specifications via conceptual analysis to automatically generate property-based tests (PBTs) for web applications. We demonstrate its application on real-world web apps and discuss future directions.
Article Search
Article: splashcomp26src-p2-p (type: Extended Abstract) doi:10.1145/3837729.3839567
SPLASH Companion '26: "Understanding Correctness ..."
Understanding Correctness Failures in Compiler Optimization
Abdullah Al Noman and Mengfei Ren
(Baylor University, USA)
Compiler optimizations improve program performance but may break program correctness when transformations fail to preserve source level semantics. This extended abstract examines optimization introduced correctness failures in GCC through bugs reported by existing C compiler testing studies. We collect bug report metadata, recover available proof of concept programs, and manually validate each program before building the testing corpus. The current dataset contains 226 analyzed GCC bugs, including 159 bugs that are directly or partially related to optimization components. Our preliminary results show that tree optimization is the primary component involved in these failures, while wrong code is the most common failure type. These findings provide an empirical basis for an optimization oriented testing framework and a reusable test suite for improving compiler optimization correctness and reliability.
Article Search
Article: splashcomp26poster-p4-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839589
SPLASH Companion '26: "bench: A Programmable Command-Line ..."
bench: A Programmable Command-Line Framework for Complex Benchmarking Workflows
Filip Říha and Filip Křikava
(Czech Technical University, Czech Republic)
Benchmarking provides much of the feedback that drives systems and language research, yet sound benchmarking is hard. As experiments grow, added programs, configurations, custom metrics, warmup, failures, and machine noise can all mislead. We present bench, a tool that keeps simple measurements simple and lets complex experiments scale without leaving a general-purpose language. It offers a command-line interface for ad-hoc runs and a small, almost declarative Python API for repeatable experiments, both backed by one engine. A builder API resolves a suite of benchmarks lazily against a typed context, so a single script can be parametrized from the command line, discover its workloads at run time, and treat process benchmarks and in-process harnesses through one pipeline. We have used it to simplify the benchmarking infrastructure for our R just-in-time compilers, to evaluate student language implementations in a course, and to drive established suites such as Renaissance and SPEC.
Article Search
Article: splashcomp26demo-p46-p (type: Short Paper) doi:10.1145/3837729.3840502
SPLASH Companion '26: "CoCoMUT: A Tool for Code-Context ..."
CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation
Alessandro Botta, Shiven Garisa, Jaya Vardhini Akurathi, Ahsanul Ameen Sabit, Trey Woodlief, and Soneya Binta Hossain
(University of Texas at Dallas, USA; Heritage High School, USA; William & Mary, USA)
Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-type information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects.
We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at type, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, type, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques.
The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99% of generated context records passed all applicable correctness checks.
Demo: https://youtu.be/RCUzkCQjG30 Artifact: https://github.com/assert-lab/CoCoMUT
Article Search
Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485
SPLASH Companion '26: "Iekkë: A Bounded-Round Partial-Order ..."
Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs
Paolo Di Biase, Bernd Fischer, Salvatore La Torre, Peter Schrammel, and Gennaro Parlato
(Gran Sasso Science Institute, Italy; Stellenbosch University, South Africa; University of Salerno, Italy; Diffblue, UK; University of Molise, Italy)
We present Iekkë, a BMC tool for verifying multi-threaded C programs. It implements a new bounded-round partial-order encoding for the sequential consistency shared-memory model. The encoding combinesbthe compactness of lazy sequentialization with the structural precision of the partial-order approach. Its concurrency constraints grow linearly in the number of shared-memory events and in the round bound 𝑘—--avoiding the quadratic/cubic blow-up of classical partial-order encodings—--and are fully propositional, enabling the use of an off-the-shelf SAT solver. Iekkë is built on top of the CBMC/Deagle infrastructure and replaces only the concurrency constraint module. It supports concurrent reachability checking, data race detection, and the usual safety property checks implemented by CBMC. Iekkë won the Bronze medal in the Concurrency category of SV-COMP 2026.
Article Search
Article: splashcomp26demo-p18-p (type: Short Paper) doi:10.1145/3837729.3840491
SPLASH Companion '26: "Phoenix: A Modular and Versatile ..."
Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis
Peisen Yao, Zinan Gu, and Qingkai Shi
(Zhejiang University, China; Nanjing University, China)
We present Phoenix, a modular pointer analysis framework for C/C++ that unifies multiple alias analysis algorithms behind a single, stable interface. Phoenix addresses the fragmentation of today’s C/C++ pointer analysis ecosystem by cleanly separating IR construction, constraint generation, solver backends, and client-facing queries—making analyses easy to compare, swap, and compose while exposing explicit precision–performance trade-offs. We evaluate two comparisons on 28 GNU coreutils programs: Phoenix-FICI versus SVF-FICI, where both analyses are flow-insensitive and context-insensitive, and Phoenix-FSCS versus SVF-FSCI, where the former is flow- and context-sensitive and the latter is flow-sensitive but context-insensitive. Phoenix-FICI is faster on all benchmarks, with a maximum speedup of 2.88×. For the second comparison, Phoenix-FSCS is faster on 13 benchmarks, slower on 14, and tied on one, with a maximum speedup of 2.91×. In production, Phoenix serves as the analysis substrate for static analysis and fuzzing tools that have uncovered hundreds of new bugs in open-source software and industrial deployments.
Article Search
Article: splashcomp26demo-p19-p (type: Short Paper) doi:10.1145/3837729.3840492
SPLASH Companion '26: "RepairFormer: Automated Repair ..."
RepairFormer: Automated Repair of Structured Inputs using Transformers
Ovi Paul, Tom J. King, and Ali Shokri
(University of Houston, USA)
Structured input files such as JSON, S-expression, DOT, OBJ, INI, and TinyC are widely used in software systems, but small corruptions can cause parsers to reject otherwise useful data. Repairing such inputs is important because malformed configuration, program, and data files can interrupt testing, analysis, deployment, and downstream automation even when most of the original content remains intact. Existing repair techniques can produce structurally valid inputs, but they often rely on deletion or repeated search, which may lose original content and result in semantic incorrectness. This paper presents RepairFormer, a transformer-based framework for structured input repair. The approach formulates repair as a supervised sequence generation task and uses format tags, oracle validation, and boundary-localized repair to generate valid outputs while preserving content. The boundary workflow focuses generation on the detected fault region, reducing the input size, and supporting repair of longer files. In evaluation, RepairFormer achieves a 88% in repair and 94% in recovery, showing strongest content preservation when repairs are successful. Additional experiments on our benchmark shows RepairFormer repairs 97.57% and recovers 94.29% with 5x faster runtime compared to state of the art.
Article Search
Artifacts Available
Article: splashcomp26demo-p37-p (type: Short Paper) doi:10.1145/3837729.3840497
SPLASH Companion '26: "CrossLangFuzzer: Differential ..."
CrossLangFuzzer: Differential Testing of Cross-Language JVM Compilers
Xiaotian Ma, Qiong Feng, Yongqiang Tian, Wei Song, and Peng Liang
(Nanjing University of Science and Technology, China; Monash University, Australia; Wuhan University, China)
Modern JVM software increasingly integrates multiple programming languages, such as Java, Kotlin, Groovy, and Scala, within a single application. Supporting such interoperability requires JVM compilers to perform cross-language compilation while reconciling subtle semantic differences across language boundaries. Errors in this process can lead to critical miscompilations, yet existing compiler testing techniques focus exclusively on isolated, single-language compilation. To address this gap, we present CrossLangFuzzer, the first differential testing framework for cross-language JVM compilation. CrossLangFuzzer leverages the Kotlin compiler's unified intermediate representation (IR) to synthesize cross language test programs. It further applies seven mutation operators to diversify generated test programs and improve bug-finding capability. Evaluated on the latest versions of five major JVM compilers, CrossLangFuzzer uncovered 32 confirmed bugs, including 15 in Kotlin, 4 in Groovy, 7 in Scala 3, 2 in Scala 2, and 4 in Java.
Article Search
Article: splashcomp26demo-p21-p (type: Short Paper) doi:10.1145/3837729.3840493
SPLASH Companion '26: "PEPPER: Native Shell Scripting ..."
PEPPER: Native Shell Scripting in Python
Ridhi Srikanth
(University of California at San Diego, USA)
Shell scripting bridges system operations and application logic by enabling programmers to concisely invoke external processes and manipulate the file system. However, for Python programmers, shell programming requires either integration of external scripts or use of libraries such as subprocess and os. This increases complexity and makes systems hard to build and debug. PEPPER extends Python by integrating persistent shell semantics directly into the language. PEPPER enables concise shell-style workflow construction while preserving seamless interoperability with Python code, libraries, and existing workflows. We will evaluate PEPPER using a benchmark of real-world shell programs, the CPython test suite, and a user study to assess its expressiveness, behavioral equivalence, and usability for Python programmers.
Article Search
Article: splashcomp26src-p5-p (type: Extended Abstract) doi:10.1145/3837729.3839570
SPLASH Companion '26: "Diffpoints: Breakpoints Comparing ..."
Diffpoints: Breakpoints Comparing Values of Variables
Filip Čmilňák, Matúš Sulír, and Milan Nosáľ
(Technical University of Košice, Slovakia; ValeSoft, Slovakia)
Debugging is an integral, yet time-consuming and cognitively demanding part of software development. While common debugging tools allow for a detailed inspection of current variable values, they do not offer a clear visualization of their evolution over time. When comparing states at different execution points, they rely on the programmer’s memory or auxiliary console outputs. In this paper, we present Diffpoints, a novel debugging tool that introduces new types of breakpoints to enable the automatic capture and comparison of variable states between multiple points of program execution. Two distinct types, namely line and group diffpoints, are supported, and to match variables from different stack traces, a heuristic is used. Diffpoints are implemented as an extension for the IntelliJ IDEA development environment. We conducted a preliminary user study and plan further evaluation.
Article Search
Article: splashcomp26demo-p35-p (type: Short Paper) doi:10.1145/3837729.3840495
SPLASH Companion '26: "OmniJinja: A Cross-Language ..."
OmniJinja: A Cross-Language VS Code Extension for Jinja Application Development
Yu Sun, Kai Gao, and Chang-ai Sun
(University of Science and Technology Beijing, China)
Jinja is one of the most widely used template engines in the Python ecosystem, enabling applications to generate documents by combining dynamic data with templates. Jinja application development is challenging because templates are polyglot artifacts and interact with backend code through implicit cross-language data contracts. However, existing tools provide limited assistance for maintaining consistency between the backend and templates. In this paper, we present OmniJinja, an event-driven VS Code extension for Jinja application development. OmniJinja performs cross-language analysis of backend Python code and Jinja templates to provide backend-aware completion, bidirectional consistency checking, and syntax diagnostics with quick fixes. A lightweight evaluation on three real-world Jinja projects demonstrates that OmniJinja effectively provides backend-aware completion and detects cross-language inconsistencies.
Article Search
Article: splashcomp26demo-p17-p (type: Short Paper) doi:10.1145/3837729.3840490
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "OmniJinja: A Cross-Language ..."
OmniJinja: A Cross-Language VS Code Extension for Jinja Application Development
Yu Sun, Kai Gao, and Chang-ai Sun
(University of Science and Technology Beijing, China)
Jinja is one of the most widely used template engines in the Python ecosystem, enabling applications to generate documents by combining dynamic data with templates. Jinja application development is challenging because templates are polyglot artifacts and interact with backend code through implicit cross-language data contracts. However, existing tools provide limited assistance for maintaining consistency between the backend and templates. In this paper, we present OmniJinja, an event-driven VS Code extension for Jinja application development. OmniJinja performs cross-language analysis of backend Python code and Jinja templates to provide backend-aware completion, bidirectional consistency checking, and syntax diagnostics with quick fixes. A lightweight evaluation on three real-world Jinja projects demonstrates that OmniJinja effectively provides backend-aware completion and detects cross-language inconsistencies.
Article Search
Article: splashcomp26demo-p17-p (type: Short Paper) doi:10.1145/3837729.3840490
SPLASH Companion '26: "Falconf: A Web-Based Tool ..."
Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis
Youyang Kim, Sahil Suneja, Yong-Hwan Jeong, Yunja Choi, Young-Woo Kwon, and Byungchul Tak
(Kyungpook National University, Republic of Korea; IBM Research, USA)
Misconfigurations continue to be one of the major causes of failures in distributed software systems, yet diagnosing them remains challenging. This is because faulty configuration parameters are difficult to identify among hundreds of configuration entries, and their effects often leave no explicit evidence in runtime logs. We present Falconf, a web-based tool for automatically diagnosing misconfigurations in distributed software systems using log analysis. Falconf takes runtime log files as input, analyzes them using a pre-trained two-stage transformer model, and produces a ranked list of suspicious configuration parameters that are likely responsible for the observed failure. The tool features an intuitive web interface that visualizes the diagnosis workflow, allowing users to select the target application and version, input log files, and inspect the ranked results without any expertise in machine learning or log analysis. We demonstrate that Falconf can effectively diagnose misconfigured parameters from real-world logs of distributed software systems, including Apache Spark and Hadoop.
Article Search
Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499
SPLASH Companion '26: "Falconf: A Web-Based Tool ..."
Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis
Youyang Kim, Sahil Suneja, Yong-Hwan Jeong, Yunja Choi, Young-Woo Kwon, and Byungchul Tak
(Kyungpook National University, Republic of Korea; IBM Research, USA)
Misconfigurations continue to be one of the major causes of failures in distributed software systems, yet diagnosing them remains challenging. This is because faulty configuration parameters are difficult to identify among hundreds of configuration entries, and their effects often leave no explicit evidence in runtime logs. We present Falconf, a web-based tool for automatically diagnosing misconfigurations in distributed software systems using log analysis. Falconf takes runtime log files as input, analyzes them using a pre-trained two-stage transformer model, and produces a ranked list of suspicious configuration parameters that are likely responsible for the observed failure. The tool features an intuitive web interface that visualizes the diagnosis workflow, allowing users to select the target application and version, input log files, and inspect the ranked results without any expertise in machine learning or log analysis. We demonstrate that Falconf can effectively diagnose misconfigured parameters from real-world logs of distributed software systems, including Apache Spark and Hadoop.
Article Search
Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499
SPLASH Companion '26: "CrossLangFuzzer: Differential ..."
CrossLangFuzzer: Differential Testing of Cross-Language JVM Compilers
Xiaotian Ma, Qiong Feng, Yongqiang Tian, Wei Song, and Peng Liang
(Nanjing University of Science and Technology, China; Monash University, Australia; Wuhan University, China)
Modern JVM software increasingly integrates multiple programming languages, such as Java, Kotlin, Groovy, and Scala, within a single application. Supporting such interoperability requires JVM compilers to perform cross-language compilation while reconciling subtle semantic differences across language boundaries. Errors in this process can lead to critical miscompilations, yet existing compiler testing techniques focus exclusively on isolated, single-language compilation. To address this gap, we present CrossLangFuzzer, the first differential testing framework for cross-language JVM compilation. CrossLangFuzzer leverages the Kotlin compiler's unified intermediate representation (IR) to synthesize cross language test programs. It further applies seven mutation operators to diversify generated test programs and improve bug-finding capability. Evaluated on the latest versions of five major JVM compilers, CrossLangFuzzer uncovered 32 confirmed bugs, including 15 in Kotlin, 4 in Groovy, 7 in Scala 3, 2 in Scala 2, and 4 in Java.
Article Search
Article: splashcomp26demo-p21-p (type: Short Paper) doi:10.1145/3837729.3840493
SPLASH Companion '26: "RepoTrace: Browser-Assisted ..."
RepoTrace: Browser-Assisted Evidence Collection for GitHub Research Datasets
Xue Yao, Zehua Zhang, Jiatong Liu, and Yongqiang Tian
(Monash University, Australia)
Empirical software engineering studies frequently build datasets from GitHub issues and pull requests. In many projects, researchers inspect pages in a browser, copy selected fields into spreadsheets, keep side notes in separate documents, and later run scripts to normalize or export the data. This workflow is flexible, but the page evidence, the research codes, and the rationale behind each decision end up spread across tabs and files, making provenance, update tracking, and multi-reviewer labeling difficult to audit.
RepoTrace is a browser-assisted research tool that collects GitHub issue and pull-request evidence into a local SQLite-backed workspace. It combines a Chrome side-panel extension, an Express backend, and a React dashboard to capture page snapshots, comments, labels, notes, screening and labeling decisions, refresh history, and scoped exports, keeping the source evidence and the research interpretation linked together.
A validation pass covered 20 Matplotlib issues across two study projects. The resulting dataset preserves 22 snapshots, 38 comments, 20 research notes, 98 annotations, 20 screening reviews, 20 fix-evidence entries, and 4 simulated unresolved consensus conflicts. The results show that RepoTrace can support a complete local evidence-collection workflow for manually constructed GitHub issue and pull-request datasets.
Article Search
Article: splashcomp26demo-p39-p (type: Short Paper) doi:10.1145/3837729.3840498
SPLASH Companion '26: "DebugTracker: Lightweight ..."
DebugTracker: Lightweight Process Evidence for Classroom Debugging
Jiatong Liu, Xue Yao, Zehua Zhang, and Yongqiang Tian
(Monash University, Australia)
Debugging exercises are often assessed from final code and test outcomes, yet these artifacts hide how students reproduced failures, formed hypotheses, inspected evidence, edited code, and verified fixes. We present DebugTracker, a Visual Studio Code extension that records lightweight debugging-process evidence for classroom tasks. DebugTracker separates uncoached Evaluation Mode traces from coached Training Mode traces, stores append-only JSONL events, and exports timeline and Markdown reports for human review. The prototype records test commands, editor and debugger metadata, student checkpoints, source snapshots, and human labels. It can also record optional image evidence and AI-assisted practice feedback. DebugTracker is largely language-agnostic: it captures process evidence through standard VS Code mechanisms rather than language-specific tooling, although debugger evidence depends on the relevant VS Code language extension. We validate the prototype with debugging tasks in Python, TypeScript, and Java, 16 automated checks, and an 11-case manual trial matrix spanning packaged VSIX installation and three operating systems.
Article Search
Article: splashcomp26demo-p43-p (type: Short Paper) doi:10.1145/3837729.3840500
SPLASH Companion '26: "LPR+: Diverse Transformations ..."
LPR+: Diverse Transformations for LLM-Aided Program Reduction
Zehua Zhang, Jiatong Liu, Xue Yao, and Yongqiang Tian
(Monash University, Australia)
Program reduction helps compiler and language-tool developers turn large failure-inducing programs into small, shareable bug reports. LPR (Large Language Models-Aided Program Reduction) demonstrated that large language models (LLMs) can complement syntax-guided reducers by proposing language-specific transformations once a generic reducer has made the input small enough for a model. However, LPR's prompt catalog contains only five broad transformation categories, leaving much of the space explored by conventional reducers implicit. We present LPR+, which makes this transformation space explicit. LPR+ keeps LPR's oracle-validated discipline, in which every candidate must still be smaller and preserve the interesting behavior, and adds thirty refined, reducer-inspired rules derived from observations of C-Reduce, Perses, and Vulcan and provided as prompts rather than trusted rewrites. On the LPR benchmark across C, Rust, and JavaScript with gpt-5.4-mini, LPR+ lowers the mean final size from 189.7 to 180.9 tokens on the cases completed by both protocols, at the cost of additional model queries. These results suggest that an explicit, oracle-validated transformation catalog provides an extension point for LLM-aided program reduction. The demonstration video is available at https://youtu.be/kNULghJH-2E.
Article Search
Article: splashcomp26demo-p48-p (type: Short Paper) doi:10.1145/3837729.3840504
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Bridging Call Boundaries: ..."
Bridging Call Boundaries: Inter-procedural Semantic Completion for Graph-Based Vulnerability Detection
Ruiguo Hu, Dongqi Wang, Shujin Yang, Zhenglin Li, and Dongming Chen
(Northeastern University, China)
Deep learning-based vulnerability detection approaches are limited when vulnerabilities involve multiple functions, where the security effect of a function depends on the behavior of invoked functions. As a result, function-level models may miss key vulnerability-related information across call boundaries. To address this issue, we propose VulSCG, a graph-based vulnerability detection framework with inter-procedural semantic completion. VulSCG first retrieves callee implementations from the corresponding project version and uses LLMs to generate structured summaries of their input, output and security-relevant behaviors. The generated summaries are injected into the caller Code Property Graph as SummaryNodes, allowing inter-procedural security semantics to participate in graph learning without expanding the full callee graph. Experiments on Devign show that VulSCG outperforms representative learning-based vulnerability detection baselines. In particular, VulSCG achieves the best F1 score on the dataset, with a F1 improvement of 4.25% over the strongest baseline. These results indicate that VulSCG improves detection effectiveness while maintaining scalability, since it complements inter-procedural semantics through compact SummaryNodes rather than full callee graph expansion.
Article Search
Article: splashcomp26poster-p5-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839590
SPLASH Companion '26: "DSLReasoning: Evaluating LLM ..."
DSLReasoning: Evaluating LLM Program Reasoning beyond Pretrained Language Familiarity
Haozhi Wang
(University of Alberta, Canada)
Large language models perform strongly on code-related tasks, but pretrained familiarity with existing programming languages can confuse whether models genuinely understand formal semantics. We introduce two synthetic domain specific languages with unfamiliar operators and modified control-flow behavior to evaluate program reasoning under reduced language familiarity. We study program execution and program equivalence checking. Preliminary experiments show strong execution performance but weaker equivalence checking correctness, suggesting that deeper semantic reasoning remains challenging for current LLMs.
Article Search
Article: splashcomp26src-p17-p (type: Extended Abstract) doi:10.1145/3837729.3839579
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "OpenRepair: An Automated Tool ..."
OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs
Jinning Zhang, Bin Yu, Haoli Zhang, Letian Wang, Wensheng Wang, and Xu Lu
(Xidian University, China)
OpenMP is a widely adopted shared-memory programming model, yet its concurrent execution is highly prone to data races, threatening software correctness and performance. Existing automated repair techniques depend heavily on manually designed synchronization strategies, which limit their applicability to diverse OpenMP programs. This paper demonstrates OpenRepair, an end-to-end automated tool designed to generate context-aware data-race fixes for OpenMP applications. OpenRepair features a robust pipeline that synergizes static analysis, retrieval-augmented generation (RAG), and large language models (LLMs). By automatically digesting runtime race reports, extracting program concurrency structures, and retrieving relevant repair knowledge, the tool seamlessly synthesizes precise, template-free patches.Evaluation on 97 OpenMP benchmarks and real-world applications highlights its scalability and practical effectiveness: OpenRepair successfully resolves 85 race conditions, improving repair capability by 44.1% over existing tools while introducing lower synchronization overhead.
Article Search
Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489
SPLASH Companion '26: "OpenRepair: An Automated Tool ..."
OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs
Jinning Zhang, Bin Yu, Haoli Zhang, Letian Wang, Wensheng Wang, and Xu Lu
(Xidian University, China)
OpenMP is a widely adopted shared-memory programming model, yet its concurrent execution is highly prone to data races, threatening software correctness and performance. Existing automated repair techniques depend heavily on manually designed synchronization strategies, which limit their applicability to diverse OpenMP programs. This paper demonstrates OpenRepair, an end-to-end automated tool designed to generate context-aware data-race fixes for OpenMP applications. OpenRepair features a robust pipeline that synergizes static analysis, retrieval-augmented generation (RAG), and large language models (LLMs). By automatically digesting runtime race reports, extracting program concurrency structures, and retrieving relevant repair knowledge, the tool seamlessly synthesizes precise, template-free patches.Evaluation on 97 OpenMP benchmarks and real-world applications highlights its scalability and practical effectiveness: OpenRepair successfully resolves 85 race conditions, improving repair capability by 44.1% over existing tools while introducing lower synchronization overhead.
Article Search
Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "CoCoMUT: A Tool for Code-Context ..."
CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation
Alessandro Botta, Shiven Garisa, Jaya Vardhini Akurathi, Ahsanul Ameen Sabit, Trey Woodlief, and Soneya Binta Hossain
(University of Texas at Dallas, USA; Heritage High School, USA; William & Mary, USA)
Software-engineering assistants often need method-level context beyond an isolated body, including enclosing-type information, documentation, callers, callees, type hierarchy, and structural characteristics. Manually collecting this context is time-consuming, inconsistent, and difficult to reproduce across large Java projects.
We present CoCoMUT, a Java tool for Code-Context Mining and Automated Dataset Generation. CoCoMUT extracts context for a focal method or generates datasets at type, package, or system scope. It discovers project structure, resolves build and classpath information, constructs a SootUp static call graph, and reconciles bytecode-level call edges with Spoon-based source extraction. Each method record combines source, type, documentation, call-graph, and metadata context, providing reproducible inputs for training and running learned software-engineering techniques.
The key contribution is a reusable, task-independent pipeline that unifies build discovery, source extraction, call-graph construction, source-bytecode reconciliation, and versioned JSON dataset generation. The resulting records can be consumed individually as context for a focal method or collectively as datasets for documentation, explanation, testing, review, repair, search, and program-comprehension workflows. We evaluate CoCoMUT on 20 real-world Java repositories evenly split between Maven and Gradle. CoCoMUT processed all 20 repositories, emitting 56,512 method-context records and 386,048 serialized call edges. Among call edges whose bytecode targets belonged to project source, CoCoMUT reconciled 97.8% to source method identities. In a manual audit of 200 randomly sampled methods across 10 systems, 99% of generated context records passed all applicable correctness checks.
Demo: https://youtu.be/RCUzkCQjG30 Artifact: https://github.com/assert-lab/CoCoMUT
Article Search
Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "Spec-Skill: A Pluggable Coding-Agent ..."
Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis
Wenjie Wu, Junjie Hu, Cheng Wen, Jialun Cao, Dugang Liu, Zhiwu Xu, Weidi Sun, Haokun Li, and Shengchao Qin
(Xidian University, China; Hong Kong University of Science and Technology, Hong Kong; Shenzhen University, China; Peking University, China)
Formal verification provides strong correctness guarantees, but its practical adoption is limited by the cost of writing precise formal specifications. While large language models can generate candidate specifications, prompt-only generation and monolithic LLM pipelines often struggle with verifier feedback, iterative repair, cross-function consistency, and project-level orchestration. Modern coding agents offer a natural interface for such tool-mediated workflows. We present Spec-Skill, a pluggable agent plugin for neuro-symbolic program specification synthesis. A host agent decomposes a C project into layered verification units and coordinates sub-agents that synthesize ACSL function contracts and loop invariants, verify them with Frama-C/WP, and repair failures using verifier feedback. A common CLI-based interface allows Spec-Skill to integrate with different coding-agent platforms, including Claude Code and Codex. We evaluate Spec-Skill on established specification-generation benchmarks and a project-scale X509-parser codebase. Spec-Skill achieves an overall Pass@5 of 98.8% across the established benchmarks and verifies 171 of 212 functions in X509-parser, demonstrating the potential of agent-oriented orchestration for project-level specification synthesis.
Article Search
Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483
SPLASH Companion '26: "ss: A Slide Description Language ..."
ss: A Slide Description Language with Dependence-Scheduled Execution
Yuchi Yamaguchi
(Institute of Science Tokyo, Japan)
Slides often include components that depend on information from across the presentation, such as tables of contents, page numbers, and figure numbers. In programmable slide descriptions, such computations can be written as queries over objects that satisfy specified conditions. To evaluate such queries correctly, all statements creating or updating objects that may be selected must already have executed. Otherwise, later additions and updates may be missed.
In this paper, we propose ss, a slide description language that orders statements according to their dependencies. ss conservatively estimates the object sets and properties read or written by each statement, and uses this information to reorder statements. As a result, document-wide computations can appear before their input objects are defined, without requiring users to manage evaluation order. To our knowledge, this is the first work to explore dependence-scheduled execution in a slide description language.
We also implemented a compiler for ss and used it in a preliminary evaluation showing that its execution model can support practical slide authoring.
Article Search
Article: splashcomp26src-p8-p (type: Extended Abstract) doi:10.1145/3837729.3839571
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Bridging Call Boundaries: ..."
Bridging Call Boundaries: Inter-procedural Semantic Completion for Graph-Based Vulnerability Detection
Ruiguo Hu, Dongqi Wang, Shujin Yang, Zhenglin Li, and Dongming Chen
(Northeastern University, China)
Deep learning-based vulnerability detection approaches are limited when vulnerabilities involve multiple functions, where the security effect of a function depends on the behavior of invoked functions. As a result, function-level models may miss key vulnerability-related information across call boundaries. To address this issue, we propose VulSCG, a graph-based vulnerability detection framework with inter-procedural semantic completion. VulSCG first retrieves callee implementations from the corresponding project version and uses LLMs to generate structured summaries of their input, output and security-relevant behaviors. The generated summaries are injected into the caller Code Property Graph as SummaryNodes, allowing inter-procedural security semantics to participate in graph learning without expanding the full callee graph. Experiments on Devign show that VulSCG outperforms representative learning-based vulnerability detection baselines. In particular, VulSCG achieves the best F1 score on the dataset, with a F1 improvement of 4.25% over the strongest baseline. These results indicate that VulSCG improves detection effectiveness while maintaining scalability, since it complements inter-procedural semantics through compact SummaryNodes rather than full callee graph expansion.
Article Search
Article: splashcomp26poster-p5-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839590
SPLASH Companion '26: "Phoenix: A Modular and Versatile ..."
Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis
Peisen Yao, Zinan Gu, and Qingkai Shi
(Zhejiang University, China; Nanjing University, China)
We present Phoenix, a modular pointer analysis framework for C/C++ that unifies multiple alias analysis algorithms behind a single, stable interface. Phoenix addresses the fragmentation of today’s C/C++ pointer analysis ecosystem by cleanly separating IR construction, constraint generation, solver backends, and client-facing queries—making analyses easy to compare, swap, and compose while exposing explicit precision–performance trade-offs. We evaluate two comparisons on 28 GNU coreutils programs: Phoenix-FICI versus SVF-FICI, where both analyses are flow-insensitive and context-insensitive, and Phoenix-FSCS versus SVF-FSCI, where the former is flow- and context-sensitive and the latter is flow-sensitive but context-insensitive. Phoenix-FICI is faster on all benchmarks, with a maximum speedup of 2.88×. For the second comparison, Phoenix-FSCS is faster on 13 benchmarks, slower on 14, and tied on one, with a maximum speedup of 2.91×. In production, Phoenix serves as the analysis substrate for static analysis and fuzzing tools that have uncovered hundreds of new bugs in open-source software and industrial deployments.
Article Search
Article: splashcomp26demo-p19-p (type: Short Paper) doi:10.1145/3837729.3840492
SPLASH Companion '26: "RepoTrace: Browser-Assisted ..."
RepoTrace: Browser-Assisted Evidence Collection for GitHub Research Datasets
Xue Yao, Zehua Zhang, Jiatong Liu, and Yongqiang Tian
(Monash University, Australia)
Empirical software engineering studies frequently build datasets from GitHub issues and pull requests. In many projects, researchers inspect pages in a browser, copy selected fields into spreadsheets, keep side notes in separate documents, and later run scripts to normalize or export the data. This workflow is flexible, but the page evidence, the research codes, and the rationale behind each decision end up spread across tabs and files, making provenance, update tracking, and multi-reviewer labeling difficult to audit.
RepoTrace is a browser-assisted research tool that collects GitHub issue and pull-request evidence into a local SQLite-backed workspace. It combines a Chrome side-panel extension, an Express backend, and a React dashboard to capture page snapshots, comments, labels, notes, screening and labeling decisions, refresh history, and scoped exports, keeping the source evidence and the research interpretation linked together.
A validation pass covered 20 Matplotlib issues across two study projects. The resulting dataset preserves 22 snapshots, 38 comments, 20 research notes, 98 annotations, 20 screening reviews, 20 fix-evidence entries, and 4 simulated unresolved consensus conflicts. The results show that RepoTrace can support a complete local evidence-collection workflow for manually constructed GitHub issue and pull-request datasets.
Article Search
Article: splashcomp26demo-p39-p (type: Short Paper) doi:10.1145/3837729.3840498
SPLASH Companion '26: "DebugTracker: Lightweight ..."
DebugTracker: Lightweight Process Evidence for Classroom Debugging
Jiatong Liu, Xue Yao, Zehua Zhang, and Yongqiang Tian
(Monash University, Australia)
Debugging exercises are often assessed from final code and test outcomes, yet these artifacts hide how students reproduced failures, formed hypotheses, inspected evidence, edited code, and verified fixes. We present DebugTracker, a Visual Studio Code extension that records lightweight debugging-process evidence for classroom tasks. DebugTracker separates uncoached Evaluation Mode traces from coached Training Mode traces, stores append-only JSONL events, and exports timeline and Markdown reports for human review. The prototype records test commands, editor and debugger metadata, student checkpoints, source snapshots, and human labels. It can also record optional image evidence and AI-assisted practice feedback. DebugTracker is largely language-agnostic: it captures process evidence through standard VS Code mechanisms rather than language-specific tooling, although debugger evidence depends on the relevant VS Code language extension. We validate the prototype with debugging tasks in Python, TypeScript, and Java, 16 automated checks, and an 11-case manual trial matrix spanning packaged VSIX installation and three operating systems.
Article Search
Article: splashcomp26demo-p43-p (type: Short Paper) doi:10.1145/3837729.3840500
SPLASH Companion '26: "LPR+: Diverse Transformations ..."
LPR+: Diverse Transformations for LLM-Aided Program Reduction
Zehua Zhang, Jiatong Liu, Xue Yao, and Yongqiang Tian
(Monash University, Australia)
Program reduction helps compiler and language-tool developers turn large failure-inducing programs into small, shareable bug reports. LPR (Large Language Models-Aided Program Reduction) demonstrated that large language models (LLMs) can complement syntax-guided reducers by proposing language-specific transformations once a generic reducer has made the input small enough for a model. However, LPR's prompt catalog contains only five broad transformation categories, leaving much of the space explored by conventional reducers implicit. We present LPR+, which makes this transformation space explicit. LPR+ keeps LPR's oracle-validated discipline, in which every candidate must still be smaller and preserve the interesting behavior, and adds thirty refined, reducer-inspired rules derived from observations of C-Reduce, Perses, and Vulcan and provided as prompts rather than trusted rewrites. On the LPR benchmark across C, Rust, and JavaScript with gpt-5.4-mini, LPR+ lowers the mean final size from 189.7 to 180.9 tokens on the cases completed by both protocols, at the cost of additional model queries. These results suggest that an explicit, oracle-validated transformation catalog provides an extension point for LLM-aided program reduction. The demonstration video is available at https://youtu.be/kNULghJH-2E.
Article Search
Article: splashcomp26demo-p48-p (type: Short Paper) doi:10.1145/3837729.3840504
SPLASH Companion '26: "OpenRepair: An Automated Tool ..."
OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs
Jinning Zhang, Bin Yu, Haoli Zhang, Letian Wang, Wensheng Wang, and Xu Lu
(Xidian University, China)
OpenMP is a widely adopted shared-memory programming model, yet its concurrent execution is highly prone to data races, threatening software correctness and performance. Existing automated repair techniques depend heavily on manually designed synchronization strategies, which limit their applicability to diverse OpenMP programs. This paper demonstrates OpenRepair, an end-to-end automated tool designed to generate context-aware data-race fixes for OpenMP applications. OpenRepair features a robust pipeline that synergizes static analysis, retrieval-augmented generation (RAG), and large language models (LLMs). By automatically digesting runtime race reports, extracting program concurrency structures, and retrieving relevant repair knowledge, the tool seamlessly synthesizes precise, template-free patches.Evaluation on 97 OpenMP benchmarks and real-world applications highlights its scalability and practical effectiveness: OpenRepair successfully resolves 85 race conditions, improving repair capability by 44.1% over existing tools while introducing lower synchronization overhead.
Article Search
Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489
SPLASH Companion '26: "FlowLog: Re-thinking Datalog ..."
FlowLog: Re-thinking Datalog for Fast and Extensible Static Analysis
Zhenghong Yu, Hangdong Zhao, Wanzhu Hou, and Paraschos Koutris
(University of Wisconsin-Madison, USA; Microsoft Gray Systems Lab, USA)
Datalog is widely used to build static analyzers, yet existing engines often force a tradeoff between efficiency and extensibility. In practice, static analyses are not run once and forgotten: users edit facts, tune rules, diagnose bottlenecks, and often need semantics beyond standard Datalog, leaving these tasks to ad hoc tooling or invasive engine rewrites.
We demonstrate FlowLog, a Datalog compiler that turns Soufflé-style programs into Differential Dataflow executables for efficient and extensible static analysis. Across 24 benchmarks derived from real-world workloads, FlowLog consistently outperforms state-of-the-art engines in runtime while remaining memory-efficient and scaling better.
The demonstration uses a DOOP points-to analysis. Attendees run it, switching the same program from one-shot to incremental evaluation that retracts a fact and updates results in milliseconds; tune it, inspecting per-operator costs in a browser-based profiler and repairing a bad join order; and extend it with a k-core example beyond standard Datalog.
Article Search
Artifacts Available
Article: splashcomp26demo-p3-p (type: Short Paper) doi:10.1145/3837729.3840480
SPLASH Companion '26: "SiRL: Signal-Level Reinforcement ..."
SiRL: Signal-Level Reinforcement Learning for Falsifying Cyber-Physical Systems
Hadiza Yusuf, Khouloud Gaaloul, and Aditi Dharmadhikari
(University of Michigan at Dearborn, USA)
Temporal logic falsification searches for inputs that cause a Cyber-Physical System to violate a Signal Temporal Logic property. Existing deep reinforcement learning (DRL) methods frame falsification as a sequential decision problem where the agent selects one input value per simulation timestep. We propose SiRL, a signal-level DRL approach that selects a complete input trajectory per simulation step and learns from the full history of interactions. Evaluated on 12 requirements of two benchmarks against two baselines, SiRL achieves the highest falsification rate on 9 of 12 benchmarks and is the only tool to falsify one unique case, while also achieving the lowest per-simulation wall-clock time across all tools.
Article Search
Article: splashcomp26poster-p3-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839588
SPLASH Companion '26: "OpenRepair: An Automated Tool ..."
OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs
Jinning Zhang, Bin Yu, Haoli Zhang, Letian Wang, Wensheng Wang, and Xu Lu
(Xidian University, China)
OpenMP is a widely adopted shared-memory programming model, yet its concurrent execution is highly prone to data races, threatening software correctness and performance. Existing automated repair techniques depend heavily on manually designed synchronization strategies, which limit their applicability to diverse OpenMP programs. This paper demonstrates OpenRepair, an end-to-end automated tool designed to generate context-aware data-race fixes for OpenMP applications. OpenRepair features a robust pipeline that synergizes static analysis, retrieval-augmented generation (RAG), and large language models (LLMs). By automatically digesting runtime race reports, extracting program concurrency structures, and retrieving relevant repair knowledge, the tool seamlessly synthesizes precise, template-free patches.Evaluation on 97 OpenMP benchmarks and real-world applications highlights its scalability and practical effectiveness: OpenRepair successfully resolves 85 race conditions, improving repair capability by 44.1% over existing tools while introducing lower synchronization overhead.
Article Search
Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489
SPLASH Companion '26: "SentryLine: Reviewable Capability ..."
SentryLine: Reviewable Capability Traces for CPython Plugin Hosts
Haoyi Zhang and Huaijin Ran
(Xi’an Jiaotong-Liverpool University, China; Nanyang Technological University, Singapore)
SentryLine makes CPython plugin admission explainable at the boundary. The host declares which authority a plugin may exercise; SentryLine records attempted authority classes and reports or rejects the first forbidden prefix before the instrumented effect is allowed to proceed. In the packaged evaluation, the combined monitor preserves all 28 benign workloads, blocks all 72 misuse workloads, and checks 13,888 boundary decisions with zero independent-contract disagreements and zero witnessless rejections. Audit-only monitoring blocks 38 of 72 misuse workloads, which is why the poster shows both interpreter-side and wrapper-side evidence. SentryLine is an admission-time review tool, not a universal Python sandbox.
Article Search
Article: splashcomp26poster-p11-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839591
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "OpenRepair: An Automated Tool ..."
OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs
Jinning Zhang, Bin Yu, Haoli Zhang, Letian Wang, Wensheng Wang, and Xu Lu
(Xidian University, China)
OpenMP is a widely adopted shared-memory programming model, yet its concurrent execution is highly prone to data races, threatening software correctness and performance. Existing automated repair techniques depend heavily on manually designed synchronization strategies, which limit their applicability to diverse OpenMP programs. This paper demonstrates OpenRepair, an end-to-end automated tool designed to generate context-aware data-race fixes for OpenMP applications. OpenRepair features a robust pipeline that synergizes static analysis, retrieval-augmented generation (RAG), and large language models (LLMs). By automatically digesting runtime race reports, extracting program concurrency structures, and retrieving relevant repair knowledge, the tool seamlessly synthesizes precise, template-free patches.Evaluation on 97 OpenMP benchmarks and real-world applications highlights its scalability and practical effectiveness: OpenRepair successfully resolves 85 race conditions, improving repair capability by 44.1% over existing tools while introducing lower synchronization overhead.
Article Search
Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "RepoTrace: Browser-Assisted ..."
RepoTrace: Browser-Assisted Evidence Collection for GitHub Research Datasets
Xue Yao, Zehua Zhang, Jiatong Liu, and Yongqiang Tian
(Monash University, Australia)
Empirical software engineering studies frequently build datasets from GitHub issues and pull requests. In many projects, researchers inspect pages in a browser, copy selected fields into spreadsheets, keep side notes in separate documents, and later run scripts to normalize or export the data. This workflow is flexible, but the page evidence, the research codes, and the rationale behind each decision end up spread across tabs and files, making provenance, update tracking, and multi-reviewer labeling difficult to audit.
RepoTrace is a browser-assisted research tool that collects GitHub issue and pull-request evidence into a local SQLite-backed workspace. It combines a Chrome side-panel extension, an Express backend, and a React dashboard to capture page snapshots, comments, labels, notes, screening and labeling decisions, refresh history, and scoped exports, keeping the source evidence and the research interpretation linked together.
A validation pass covered 20 Matplotlib issues across two study projects. The resulting dataset preserves 22 snapshots, 38 comments, 20 research notes, 98 annotations, 20 screening reviews, 20 fix-evidence entries, and 4 simulated unresolved consensus conflicts. The results show that RepoTrace can support a complete local evidence-collection workflow for manually constructed GitHub issue and pull-request datasets.
Article Search
Article: splashcomp26demo-p39-p (type: Short Paper) doi:10.1145/3837729.3840498
SPLASH Companion '26: "DebugTracker: Lightweight ..."
DebugTracker: Lightweight Process Evidence for Classroom Debugging
Jiatong Liu, Xue Yao, Zehua Zhang, and Yongqiang Tian
(Monash University, Australia)
Debugging exercises are often assessed from final code and test outcomes, yet these artifacts hide how students reproduced failures, formed hypotheses, inspected evidence, edited code, and verified fixes. We present DebugTracker, a Visual Studio Code extension that records lightweight debugging-process evidence for classroom tasks. DebugTracker separates uncoached Evaluation Mode traces from coached Training Mode traces, stores append-only JSONL events, and exports timeline and Markdown reports for human review. The prototype records test commands, editor and debugger metadata, student checkpoints, source snapshots, and human labels. It can also record optional image evidence and AI-assisted practice feedback. DebugTracker is largely language-agnostic: it captures process evidence through standard VS Code mechanisms rather than language-specific tooling, although debugger evidence depends on the relevant VS Code language extension. We validate the prototype with debugging tasks in Python, TypeScript, and Java, 16 automated checks, and an 11-case manual trial matrix spanning packaged VSIX installation and three operating systems.
Article Search
Article: splashcomp26demo-p43-p (type: Short Paper) doi:10.1145/3837729.3840500
SPLASH Companion '26: "LPR+: Diverse Transformations ..."
LPR+: Diverse Transformations for LLM-Aided Program Reduction
Zehua Zhang, Jiatong Liu, Xue Yao, and Yongqiang Tian
(Monash University, Australia)
Program reduction helps compiler and language-tool developers turn large failure-inducing programs into small, shareable bug reports. LPR (Large Language Models-Aided Program Reduction) demonstrated that large language models (LLMs) can complement syntax-guided reducers by proposing language-specific transformations once a generic reducer has made the input small enough for a model. However, LPR's prompt catalog contains only five broad transformation categories, leaving much of the space explored by conventional reducers implicit. We present LPR+, which makes this transformation space explicit. LPR+ keeps LPR's oracle-validated discipline, in which every candidate must still be smaller and preserve the interesting behavior, and adds thirty refined, reducer-inspired rules derived from observations of C-Reduce, Perses, and Vulcan and provided as prompts rather than trusted rewrites. On the LPR benchmark across C, Rust, and JavaScript with gpt-5.4-mini, LPR+ lowers the mean final size from 189.7 to 180.9 tokens on the cases completed by both protocols, at the cost of additional model queries. These results suggest that an explicit, oracle-validated transformation catalog provides an extension point for LLM-aided program reduction. The demonstration video is available at https://youtu.be/kNULghJH-2E.
Article Search
Article: splashcomp26demo-p48-p (type: Short Paper) doi:10.1145/3837729.3840504
SPLASH Companion '26: "FlowLog: Re-thinking Datalog ..."
FlowLog: Re-thinking Datalog for Fast and Extensible Static Analysis
Zhenghong Yu, Hangdong Zhao, Wanzhu Hou, and Paraschos Koutris
(University of Wisconsin-Madison, USA; Microsoft Gray Systems Lab, USA)
Datalog is widely used to build static analyzers, yet existing engines often force a tradeoff between efficiency and extensibility. In practice, static analyses are not run once and forgotten: users edit facts, tune rules, diagnose bottlenecks, and often need semantics beyond standard Datalog, leaving these tasks to ad hoc tooling or invasive engine rewrites.
We demonstrate FlowLog, a Datalog compiler that turns Soufflé-style programs into Differential Dataflow executables for efficient and extensible static analysis. Across 24 benchmarks derived from real-world workloads, FlowLog consistently outperforms state-of-the-art engines in runtime while remaining memory-efficient and scaling better.
The demonstration uses a DOOP points-to analysis. Attendees run it, switching the same program from one-shot to incremental evaluation that retracts a fact and updates results in milliseconds; tune it, inspecting per-operator costs in a browser-based profiler and repairing a bad join order; and extend it with a k-core example beyond standard Datalog.
Article Search
Artifacts Available
Article: splashcomp26demo-p3-p (type: Short Paper) doi:10.1145/3837729.3840480
SPLASH Companion '26: "Accurate Specification Recovery ..."
Accurate Specification Recovery for Effective Test Generation
Junda Zhao
(University of Toronto, Canada)
Large language model (LLM)-based unit-test generation has largely been studied under the assumption that the code under test is correct, using coverage or test-correctness metrics that do not directly measure defect detection. When the code under test is buggy, however, models can be guided toward assertions that encode the faulty behavior, producing tests that confirm rather than reveal defects. Our recent work quantified this misguidance effect and showed that a specification-based approach, which first recovers a behavioral specification of the focal method from its buggy implementation and then generates tests from that specification, can substantially mitigate it. Although this establishes a specification-recovery-first paradigm for LLM-based unit-test generation, the recovery step itself remains simple and its specifications are themselves fallible. This dissertation therefore aims to make specification recovery from imperfect code accurate, evidence-driven, and uncertainty-aware, so that it consistently yields effective bug-finding tests.
Article Search
Article: splashcomp26doc-p31-p (type: Extended Abstract) doi:10.1145/3837729.3842146
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503
SPLASH Companion '26: "SemaPLC: An Open-Source Agentic ..."
SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language
Yanlun Tu, Huacan Wang, Ziyue Zhou, Jie Zhou, Ningyan Zhu, Ge Chen, Wangyi Chen, Xiaofeng Mou, Tengfei Zhou, Dasheng Yang, Hui Zhang, and Yi Xu
(Midea AIRC, China; KUKA, China; Zhejiang University, China; KUKA, Germany)
Programmable logic controllers (PLCs) run much of the world's industrial automation, but writing and validating their IEC~61131-3 Structured Text (ST) is time-consuming and expert-intensive. Large language models (LLMs) can draft ST from a natural-language description, but existing open-source PLC editors give users no way to check that the generated program behaves as specified, or to simulate it before deployment. We present SemaPLC, an open-source IDE that closes this gap. From a natural-language description, a model-agnostic LLM agent drafts ST and SemaPLC runs a closed loop over it: it compiles, deploys, and verifies the user's scenarios into a pass/fail behavioral report, repairing the code from feedbacks until it compiles and every scenario passes. It then renders a live in-browser process simulation alongside the ST source, an automatically derived ladder view, and real-time variables, all in synchronized panels. SemaPLC ships as two reusable open-source components, a web IDE and a PLC tool suite. Across classic control scenarios, SemaPLC turns natural-language prompts into behaviorally verified and simulated programs, putting a trustworthy, hardware-free PLC programming agent into a single browser tab.
Article Search
Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496
SPLASH Companion '26: "Sema Core: An Open, Embeddable ..."
Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond
Huacan Wang, Jie Zhou, Ningyan Zhu, Shuo Zhang, Yanlun Tu, Feiyu Chen, Jiarou Wu, Ziyue Zhou, Ge Chen, Chen Liu, Wangyi Chen, Xiaofeng Mou, and Yi Xu
(Midea AIRC, China)
AI coding agents are increasingly used in software development, but most are delivered as integrated applications whose reasoning logic is tied to a specific interface, model provider, and deployment setting. This coupling makes it difficult for researchers and tool builders to reuse agent capabilities across different developer tools, workflows, and deployment environments. We present Sema Core, an open, embeddable AI coding agent runtime that is decoupled from any particular client and distributed as a standalone npm package. Through a compact API and typed event stream, Sema Core allows different clients to reuse the same reasoning loop, tool system, permissions, background tasks, Skills/MCP integration, and model adapters. We demonstrate the Sema Core runtime through Sema Code, a flagship VSCode extension built as a thin UI client, and additional clients including a multi-channel assistant and an industrial programming assistant. We provide source code, documentation, a demo video, and an archived release.
Article Search
Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503