SPLASH 2026 – Companion Proceedings

Frontmatter

SPLASH/ISSTA Keynotes

SPLASH Keynotes

In the Age of AI Coding Agents, Keeping the Engineer in Software Engineering (Keynote)
Elena Glassman
(Harvard University, USA)
There appears to be two distinct camps gathering steam as AI coding agents get increasingly adept at generating software on the basis of some light natural language specifications: those who want to maximally remove the ‘error-prone’ sentient bags of mostly water at the keyboard and those who stubbornly assert their own relevance as their AI-enhanced coding interfaces run off and make significant (but also often not-quite-right) contributions to the code base without even checking in. I fall into the latter camp, and in this talk, I’ll make the case for why the former camp is completely wrong—as long as we invest in designing the interfaces necessary to give our sentient water bag selves meaningful oversight and agency. Perhaps even more importantly, these interfaces might help preserve the meaning that brought us to this field in the first place: building up (rather than eroding) our understanding of the systems, languages, and software applications that fascinate us when our context allows for or demands it.
@InProceedings{SPLASH26p1, author = {Elena Glassman}, title = {In the Age of AI Coding Agents, Keeping the Engineer in Software Engineering (Keynote)}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {1-1}, doi = {10.1145/3837729.3850161}, year = {2026}, } Publisher's Version Article: splashcomp26key-key1-p (type: Keynote) doi:10.1145/3837729.3850161

Mojo: Towards One Systems Language for All Hardware (Keynote)
Chris Lattner
(Modular AI, USA)
Compute is becoming more heterogeneous, and programming it currently means juggling various languages and libraries in one project (e.g. Python, PyTorch, Triton, and CUDA ). The goal of Mojo is to provide a single system language for an heterogeneous era. This talk focuses on two foundations of Mojo: parametric metaprogramming and an ownership model built on origins, and the open language design problems that remain to be solved.
@InProceedings{SPLASH26p2, author = {Chris Lattner}, title = {Mojo: Towards One Systems Language for All Hardware (Keynote)}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {2-2}, doi = {10.1145/3837729.3850162}, year = {2026}, } Publisher's Version Article: splashcomp26key-key2-p (type: Keynote) doi:10.1145/3837729.3850162

The Augmented Forest (Keynote)
Kent Beck
(KentBeck.com, USA)
As AI genies make programming more joyful in some ways, more fraught in others, how can we as individuals and teams adapt? How can we track a rapidly changing landscape of tools and still get stuff done? How can we communicate our new powers, strengths and weaknesses, to those without direct experience of programming? The Forest & Desert is a dialectical framing of software development as either resource-rich and resource replenishing or continually near starvation. The genie promises to intensify both experiences.
@InProceedings{SPLASH26p3, author = {Kent Beck}, title = {The Augmented Forest (Keynote)}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {3-3}, doi = {10.1145/3837729.3850163}, year = {2026}, } Publisher's Version Article: splashcomp26key-key3-p (type: Keynote) doi:10.1145/3837729.3850163

ISSTA Keynotes

Beyond Next-Token Prediction: Autonomous Verification and Visual Testing in the Agent-First Era (Keynote)
Paige Bailey
(Google, USA)
Generative models for code have rapidly evolved from simple autocomplete tools into autonomous software engineering agents capable of navigating complex repositories and synthesizing multi-file patches. However, as these models take on more ambitious tasks, the fundamental bottleneck is no longer generating code – it is rigorous validation, end-to-end verification, and testing.
In this talk, we explore how agent-first development platforms like Google Antigravity shift the paradigm from manual test authoring to autonomous software verification. Rather than relying solely on static analysis or brittle, hardcoded UI scripts, we discuss how autonomous agents can be orchestrated to continuously test and validate software applications against dynamic real-world environments.
We provide an overview of how execution-based feedback, automated test generation, and browser-in-the-loop agents integrate directly into development workflows. More specifically, we describe recent advances in autonomous visual testing – where sandboxed browser subagents interact with live user interfaces, capture visual artifacts (such as video recordings and state screenshots), and reason about functional and UI regressions just as a human QA engineer would. Finally, we examine how verifiable agent deliverables and automated exploration are closing the loop between generative code synthesis and industrial-grade software reliability.
@InProceedings{SPLASH26p4, author = {Paige Bailey}, title = {Beyond Next-Token Prediction: Autonomous Verification and Visual Testing in the Agent-First Era (Keynote)}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {4-4}, doi = {10.1145/3837729.3850164}, year = {2026}, } Publisher's Version Article: splashcomp26key-key4-p (type: Keynote) doi:10.1145/3837729.3850164

Finding the Bugs Users Would Find: From Sapienz to Autonomous Agents (Keynote)
Ke Mao
(Meta, UK)
This keynote accompanies the ISSTA 2026 Impact Paper Award for the paper “Sapienz: Multi-objective Automated Testing for Android Applications”, first presented in 2016. Sapienz recast user-interface test generation as a multi-objective search, raising coverage and fault revelation while minimising the length of each failing sequence, so that every reported failure came with a short, replayable witness. Applied to the 1,000 most popular Google Play apps, it revealed 558 previously unknown crashes. The guiding principle: automated testing earns its place only when its results are actionable.
What followed was an unusually rapid move from prototype to industrial scale: about three months from publication to the founding of the startup Majicke (acquired by Facebook), and Facebook-scale deployment in 17 months, into continuous integration at Meta, where Sapienz has tested changes, as they are committed to the repository, for the Facebook, Messenger, Instagram, and WhatsApp apps ever since. Today it runs around 2.5 million tests a day across these apps, surfaces roughly 2,000 unique crashes a week, and helps safeguard around 200 app releases a month, thereby ensuring high product reliability and quality.
Its reach quickly outgrew crash-finding. Because it generates realistic yet privacy-safe user interactions, Sapienz became the app-exploration engine for dynamic taint analysis at WhatsApp; within the PrivacyCAT system it shifts privacy protection left, helping detect the majority of in-scope privacy incidents before release and safeguarding the privacy of more than two billion users.
The talk closes on what Sapienz could not do: judge whether observed behaviour is correct (the oracle problem). Large language model agents can now explore an app and reason about whether behaviour matches what a user should expect, extending automated testing from reliability to functional correctness and, increasingly, to automated repair. Sapienz’s core ideas, multi-objective exploration and actionable fault revelation, carry over directly. A decade on, that founding principle still holds true.
@InProceedings{SPLASH26p5, author = {Ke Mao}, title = {Finding the Bugs Users Would Find: From Sapienz to Autonomous Agents (Keynote)}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {5-5}, doi = {10.1145/3837729.3850165}, year = {2026}, } Publisher's Version Article: splashcomp26key-key5-p (type: Keynote) doi:10.1145/3837729.3850165

Joint SPLASH/ISSTA Doctoral Symposium

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.
@InProceedings{SPLASH26p6, author = {Zain K Aamer}, title = {Property-Based Testing of Separation Logic Specifications}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {6-8}, doi = {10.1145/3837729.3842144}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p5-p (type: Extended Abstract) doi:10.1145/3837729.3842144

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.
@InProceedings{SPLASH26p9, author = {Haonan Li}, title = {After the Hitchhiker’s Guide: Toward Principled LLM Assistance for Static Analysis}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {9-11}, doi = {10.1145/3837729.3842145}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p18-p (type: Extended Abstract) doi:10.1145/3837729.3842145

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.
@InProceedings{SPLASH26p12, author = {Junda Zhao}, title = {Accurate Specification Recovery for Effective Test Generation}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {12-14}, doi = {10.1145/3837729.3842146}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p31-p (type: Extended Abstract) doi:10.1145/3837729.3842146

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.
@InProceedings{SPLASH26p15, author = {Hang Du}, title = {The Mechanisms and Practice of Mutation Testing in Improving Software Quality}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {15-17}, doi = {10.1145/3837729.3842147}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p57-p (type: Extended Abstract) doi:10.1145/3837729.3842147

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.
@InProceedings{SPLASH26p18, author = {Karuna Grewal}, title = {Safe<T>: Automaton-Theoretic Runtime Monitoring of Blackbox Distributed Systems}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {18-20}, doi = {10.1145/3837729.3842148}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p86-p (type: Extended Abstract) doi:10.1145/3837729.3842148

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.
@InProceedings{SPLASH26p21, author = {Victor Chen}, title = {Towards Scalable and Verifiable Automated Translation from C to Safe Rust}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {21-23}, doi = {10.1145/3837729.3842149}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p96-p (type: Extended Abstract) doi:10.1145/3837729.3842149

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.
@InProceedings{SPLASH26p24, author = {Erfan Arvan}, title = {Toward Reliable Automatic Proxies for Code Comprehensibility}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {24-26}, doi = {10.1145/3837729.3842150}, year = {2026}, } Publisher's Version Article: splashcomp26doc-p99-p (type: Extended Abstract) doi:10.1145/3837729.3842150

Joint SPLASH/ISSTA Student Research Competition

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.
@InProceedings{SPLASH26p27, author = {Savitha Ravi}, title = {Generating Property-Based Tests for Web Applications}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {27-29}, doi = {10.1145/3837729.3839567}, year = {2026}, } Publisher's Version Article: splashcomp26src-p2-p (type: Extended Abstract) doi:10.1145/3837729.3839567

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.
@InProceedings{SPLASH26p30, author = {Aila Jahromi and Junhao Gao and Zhixuan He and Jonathan Mendoza}, title = {OLIVE: Output-Level Iterative Verification Engine}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {30-32}, doi = {10.1145/3837729.3839568}, year = {2026}, } Publisher's Version Article: splashcomp26src-p3-p (type: Extended Abstract) doi:10.1145/3837729.3839568

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.
@InProceedings{SPLASH26p33, author = {Binamra Aryal}, title = {Single-Metric Size and Complexity Thresholds Fail to Forecast Refactoring}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {33-35}, doi = {10.1145/3837729.3839569}, year = {2026}, } Publisher's Version Article: splashcomp26src-p4-p (type: Extended Abstract) doi:10.1145/3837729.3839569

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.
@InProceedings{SPLASH26p36, author = {Ridhi Srikanth}, title = {PEPPER: Native Shell Scripting in Python}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {36-38}, doi = {10.1145/3837729.3839570}, year = {2026}, } Publisher's Version Article: splashcomp26src-p5-p (type: Extended Abstract) doi:10.1145/3837729.3839570

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.
@InProceedings{SPLASH26p39, author = {Yuchi Yamaguchi}, title = {ss: A Slide Description Language with Dependence-Scheduled Execution}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {39-41}, doi = {10.1145/3837729.3839571}, year = {2026}, } Publisher's Version Article: splashcomp26src-p8-p (type: Extended Abstract) doi:10.1145/3837729.3839571

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.
@InProceedings{SPLASH26p42, author = {Giacomo Boldini}, title = {Modular Abstract Interpretation for Stack-Heap Analysis of C/C++ via LLVM IR}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {42-44}, doi = {10.1145/3837729.3839572}, year = {2026}, } Publisher's Version Article: splashcomp26src-p9-p (type: Extended Abstract) doi:10.1145/3837729.3839572

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.
@InProceedings{SPLASH26p45, author = {Jack Le}, title = {Do Machines Struggle Where Humans Do? Obfuscation as a Probe of Human and Machine Code Comprehension}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {45-46}, doi = {10.1145/3837729.3839573}, year = {2026}, } Publisher's Version Article: splashcomp26src-p10-p (type: Extended Abstract) doi:10.1145/3837729.3839573

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.
@InProceedings{SPLASH26p47, author = {Lu Maltsis}, title = {Typed Template Fuzzing}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {47-49}, doi = {10.1145/3837729.3839574}, year = {2026}, } Publisher's Version Article: splashcomp26src-p11-p (type: Extended Abstract) doi:10.1145/3837729.3839574

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.
@InProceedings{SPLASH26p50, author = {Aisha Gurbanli}, title = {ActionTaint: Framework-Aware Taint Analysis for Next.js Server Actions}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {50-52}, doi = {10.1145/3837729.3839575}, year = {2026}, } Publisher's Version Article: splashcomp26src-p12-p (type: Extended Abstract) doi:10.1145/3837729.3839575

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.
@InProceedings{SPLASH26p53, author = {Erfan Arvan}, title = {Template-Free Dynamic Invariant Detection}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {53-55}, doi = {10.1145/3837729.3839576}, year = {2026}, } Publisher's Version Article: splashcomp26src-p13-p (type: Extended Abstract) doi:10.1145/3837729.3839576

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).
@InProceedings{SPLASH26p56, author = {Muhammad Hassan}, title = {ThunderFork: Splitting SMT Queries with Targeted Control-Flow Transformations}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {56-58}, doi = {10.1145/3837729.3839577}, year = {2026}, } Publisher's Version Article: splashcomp26src-p14-p (type: Extended Abstract) doi:10.1145/3837729.3839577

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 f_max degradation from the deepening winner-selection network. Throughput efficiency and area efficiency diverge: f_max retention falls monotonically while speedup per LUT rises, peaks near 8.22×10⁻⁴ 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.
@InProceedings{SPLASH26p59, author = {Andrew Bonilla}, title = {How Far Does Replication Pay Off? A Throughput-Area Study of Brute-Force SAT on an ECP5 FPGA}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {59-61}, doi = {10.1145/3837729.3839578}, year = {2026}, } Publisher's Version Article: splashcomp26src-p15-p (type: Extended Abstract) doi:10.1145/3837729.3839578

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.
@InProceedings{SPLASH26p62, author = {Haozhi Wang}, title = {DSLReasoning: Evaluating LLM Program Reasoning beyond Pretrained Language Familiarity}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {62-64}, doi = {10.1145/3837729.3839579}, year = {2026}, } Publisher's Version Article: splashcomp26src-p17-p (type: Extended Abstract) doi:10.1145/3837729.3839579

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.
@InProceedings{SPLASH26p65, author = {Zenas Boamah}, title = {Measuring Per-Decision Propagation Work as a Formula-Dependent Signal}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {65-67}, doi = {10.1145/3837729.3839581}, year = {2026}, } Publisher's Version Article: splashcomp26src-p19-p (type: Extended Abstract) doi:10.1145/3837729.3839581

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.
@InProceedings{SPLASH26p68, author = {Ye Liu}, title = {Detecting Silent Java GC Bugs via Anomalous Runtime Behavior}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {68-70}, doi = {10.1145/3837729.3839582}, year = {2026}, } Publisher's Version Article: splashcomp26src-p20-p (type: Extended Abstract) doi:10.1145/3837729.3839582

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.
@InProceedings{SPLASH26p71, author = {Mushfiqur Rahman Chowdhury}, title = {Slice-Guided, Context-Augmented Large Language Model Inference of Java Nullability Annotations}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {71-73}, doi = {10.1145/3837729.3839583}, year = {2026}, } Publisher's Version Article: splashcomp26src-p21-p (type: Extended Abstract) doi:10.1145/3837729.3839583

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.
@InProceedings{SPLASH26p74, author = {Md Khairul Azman}, title = {Knowing When a Cheap Model Is Enough: An Information Limit on Pre-review Cost Routing for LLM Code Review}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {74-76}, doi = {10.1145/3837729.3839585}, year = {2026}, } Publisher's Version Article: splashcomp26src-p24-p (type: Extended Abstract) doi:10.1145/3837729.3839585

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.
@InProceedings{SPLASH26p77, author = {Niv Benaloul}, title = {Code as Interface for No-Code}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {77-79}, doi = {10.1145/3837729.3839586}, year = {2026}, } Publisher's Version Article: splashcomp26src-p25-p (type: Extended Abstract) doi:10.1145/3837729.3839586

Joint SPLASH/ISSTA Tool Demonstrations

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.
@InProceedings{SPLASH26p80, author = {Sachin Gupta}, title = {HeapLens: An IDE-Integrated Tool for Heap Dump Analysis with In-Editor Source Bridging and LLM-Assisted Diagnosis}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {80-84}, doi = {10.1145/3837729.3840479}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p1-p (type: Short Paper) doi:10.1145/3837729.3840479

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.
@InProceedings{SPLASH26p85, author = {Zhenghong Yu and Hangdong Zhao and Wanzhu Hou and Paraschos Koutris}, title = {FlowLog: Re-thinking Datalog for Fast and Extensible Static Analysis}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {85-90}, doi = {10.1145/3837729.3840480}, year = {2026}, } Publisher's Version Published Artifact Artifacts Available Article: splashcomp26demo-p3-p (type: Short Paper) doi:10.1145/3837729.3840480

flowlog-rs/flowlog: ISSTA/SPLASH 2026 Tool Demo Artifact (doi:10.5281/zenodo.20815412): Artifact snapshot for the FlowLog tool demonstration submission to the ISSTA/SPLASH 2026 Tool Demonstration Track. FlowLog compiles Soufflé-style Datalog programs into standalone Differential Dataflow executables and supports efficient one-shot execution, incremental maintenance, profiling, and extended semantics. The ...

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.
@InProceedings{SPLASH26p91, author = {Joonghoon Lee and Nicolas Klose and Seokhyun Lee and Peter Müller and Hakjoo Oh}, title = {Fusion: A Fold and Unfold Annotation Synthesis Tool for Viper-Based Verification}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {91-96}, doi = {10.1145/3837729.3840481}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p4-p (type: Short Paper) doi:10.1145/3837729.3840481

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.
@InProceedings{SPLASH26p97, author = {Alastair F. Donaldson and James Lee-Jones and Jonathan Foo}, title = {Dredd: Scalable Source-Level Mutation Testing for Large C/C++ Codebases}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {97-101}, doi = {10.1145/3837729.3840482}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p6-p (type: Short Paper) doi:10.1145/3837729.3840482

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.
@InProceedings{SPLASH26p102, author = {Wenjie Wu and Junjie Hu and Cheng Wen and Jialun Cao and Dugang Liu and Zhiwu Xu and Weidi Sun and Haokun Li and Shengchao Qin}, title = {Spec-Skill: A Pluggable Coding-Agent Plugin for Neuro-symbolic Program Specification Synthesis}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {102-107}, doi = {10.1145/3837729.3840483}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p7-p (type: Short Paper) doi:10.1145/3837729.3840483

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.
@InProceedings{SPLASH26p108, author = {Mahmoud Khawaja}, title = {Query Analyzer: Framework-Agnostic, Confidence-Based N+1 Detection for the JVM}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {108-113}, doi = {10.1145/3837729.3840484}, year = {2026}, } Publisher's Version Published Artifact Artifacts Available Article: splashcomp26demo-p8-p (type: Short Paper) doi:10.1145/3837729.3840484

Reproduction Package for Article `Query Analyzer: Framework-Agnostic, Confidence-Based N+1 Detection for the JVM' (doi:10.5281/zenodo.21997091): Query Analyzer is a framework-agnostic N+1 query detector and query-plan analyzer for the JVM. This package contains the complete tool source, the benchmark module used for every experiment reported in the paper, and the PetClinic and many-to-many case studies. Components: - query-analyzer-core: the detection engine ...

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
@InProceedings{SPLASH26p114, author = {Alessandro Botta and Shiven Garisa and Jaya Vardhini Akurathi and Ahsanul Ameen Sabit and Trey Woodlief and Soneya Binta Hossain}, title = {CoCoMUT: A Tool for Code-Context Mining and Automated Dataset Generation}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {114-119}, doi = {10.1145/3837729.3840485}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p9-p (type: Short Paper) doi:10.1145/3837729.3840485

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.
@InProceedings{SPLASH26p120, author = {Michał Andryskowski and Amber Gorzynski and Hasan Mohsin and Alastair F. Donaldson}, title = {WGSLsmith: Randomised Testing for the WebGPU Shading Language}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {120-125}, doi = {10.1145/3837729.3840486}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p10-p (type: Short Paper) doi:10.1145/3837729.3840486

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.
@InProceedings{SPLASH26p126, author = {Chin Khor and Robyn Lutz and Amir Niaraki}, title = {VarCHEKER: A Variability-Based Static Analyzer for Python Applications}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {126-131}, doi = {10.1145/3837729.3840487}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p11-p (type: Short Paper) doi:10.1145/3837729.3840487

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.
@InProceedings{SPLASH26p132, author = {Yidi Kao and Shawn Burnham and Tommi Rose Fahy and Ali Ghanbari}, title = {ADEPT: A Unified Framework for Deep Learning Test Adequacy}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {132-137}, doi = {10.1145/3837729.3840488}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p14-p (type: Short Paper) doi:10.1145/3837729.3840488

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.
@InProceedings{SPLASH26p138, author = {Jinning Zhang and Bin Yu and Haoli Zhang and Letian Wang and Wensheng Wang and Xu Lu}, title = {OpenRepair: An Automated Tool for OpenMP Data Race Repair via Retrieval-Augmented LLMs}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {138-143}, doi = {10.1145/3837729.3840489}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p16-p (type: Short Paper) doi:10.1145/3837729.3840489

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.
@InProceedings{SPLASH26p144, author = {Yu Sun and Kai Gao and Chang-ai Sun}, title = {OmniJinja: A Cross-Language VS Code Extension for Jinja Application Development}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {144-149}, doi = {10.1145/3837729.3840490}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p17-p (type: Short Paper) doi:10.1145/3837729.3840490

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 combines the 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.
@InProceedings{SPLASH26p150, author = {Paolo Di Biase and Bernd Fischer and Salvatore La Torre and Peter Schrammel and Gennaro Parlato}, title = {Iekkë: A Bounded-Round Partial-Order Encoding Verification Tool for Concurrent C Programs}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {150-155}, doi = {10.1145/3837729.3840491}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p18-p (type: Short Paper) doi:10.1145/3837729.3840491

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.
@InProceedings{SPLASH26p156, author = {Peisen Yao and Zinan Gu and Qingkai Shi}, title = {Phoenix: A Modular and Versatile Framework for C/C++ Pointer Analysis}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {156-161}, doi = {10.1145/3837729.3840492}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p19-p (type: Short Paper) doi:10.1145/3837729.3840492

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.
@InProceedings{SPLASH26p162, author = {Xiaotian Ma and Qiong Feng and Yongqiang Tian and Wei Song and Peng Liang}, title = {CrossLangFuzzer: Differential Testing of Cross-Language JVM Compilers}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {162-167}, doi = {10.1145/3837729.3840493}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p21-p (type: Short Paper) doi:10.1145/3837729.3840493

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.
@InProceedings{SPLASH26p168, author = {Laura Plein and Matthieu Jimenez and Mike Papadakis}, title = {PyMut4SE: Comprehensive Mutation Testing for Python}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {168-173}, doi = {10.1145/3837729.3840494}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p34-p (type: Short Paper) doi:10.1145/3837729.3840494

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.
@InProceedings{SPLASH26p174, author = {Filip Čmilňák and Matúš Sulír and Milan Nosáľ}, title = {Diffpoints: Breakpoints Comparing Values of Variables}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {174-179}, doi = {10.1145/3837729.3840495}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p35-p (type: Short Paper) doi:10.1145/3837729.3840495

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.
@InProceedings{SPLASH26p180, author = {Yanlun Tu and Huacan Wang and Ziyue Zhou and Jie Zhou and Ningyan Zhu and Ge Chen and Wangyi Chen and Xiaofeng Mou and Tengfei Zhou and Dasheng Yang and Hui Zhang and Yi Xu}, title = {SemaPLC: An Open-Source Agentic IDE for Generation, Verification, and Simulation of PLC Programs from Natural Language}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {180-185}, doi = {10.1145/3837729.3840496}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p36-p (type: Short Paper) doi:10.1145/3837729.3840496

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.
@InProceedings{SPLASH26p186, author = {Ovi Paul and Tom J. King and Ali Shokri}, title = {RepairFormer: Automated Repair of Structured Inputs using Transformers}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {186-191}, doi = {10.1145/3837729.3840497}, year = {2026}, } Publisher's Version Published Artifact Artifacts Available Article: splashcomp26demo-p37-p (type: Short Paper) doi:10.1145/3837729.3840497

RepairFormer: Automated Repair of Structured Inputs Using Transformers (doi:10.5281/zenodo.20956508): The artifact contains the source code, scripts, oracle, and example data required to train, evaluate, and demonstrate RepairFormer. It includes scripts for data collection, input mutation, boundary data conversion, dataset splitting, model training, and inference. The artifact also provides parser based oracles for ...

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.
@InProceedings{SPLASH26p192, author = {Xue Yao and Zehua Zhang and Jiatong Liu and Yongqiang Tian}, title = {RepoTrace: Browser-Assisted Evidence Collection for GitHub Research Datasets}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {192-197}, doi = {10.1145/3837729.3840498}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p39-p (type: Short Paper) doi:10.1145/3837729.3840498

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.
@InProceedings{SPLASH26p198, author = {Youyang Kim and Sahil Suneja and Yong-Hwan Jeong and Yunja Choi and Young-Woo Kwon and Byungchul Tak}, title = {Falconf: A Web-Based Tool for Misconfiguration Diagnosis via Log Analysis}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {198-202}, doi = {10.1145/3837729.3840499}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p41-p (type: Short Paper) doi:10.1145/3837729.3840499

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.
@InProceedings{SPLASH26p203, author = {Jiatong Liu and Xue Yao and Zehua Zhang and Yongqiang Tian}, title = {DebugTracker: Lightweight Process Evidence for Classroom Debugging}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {203-208}, doi = {10.1145/3837729.3840500}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p43-p (type: Short Paper) doi:10.1145/3837729.3840500

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.
@InProceedings{SPLASH26p209, author = {Myungho Lee and Seokhyeon Moon and Yoon-Chan Jhi and Hakjoo Oh}, title = {SCOUT: A Scenario-Guided Unit Test Generation Tool for Compact Open-Source LLMs}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {209-214}, doi = {10.1145/3837729.3840501}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p44-p (type: Short Paper) doi:10.1145/3837729.3840501

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.
@InProceedings{SPLASH26p215, author = {Filip Říha and Filip Křikava}, title = {bench: A Programmable Command-Line Framework for Complex Benchmarking Workflows}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {215-219}, doi = {10.1145/3837729.3840502}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p46-p (type: Short Paper) doi:10.1145/3837729.3840502

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.
@InProceedings{SPLASH26p220, author = {Huacan Wang and Jie Zhou and Ningyan Zhu and Shuo Zhang and Yanlun Tu and Feiyu Chen and Jiarou Wu and Ziyue Zhou and Ge Chen and Chen Liu and Wangyi Chen and Xiaofeng Mou and Yi Xu}, title = {Sema Core: An Open, Embeddable AI Coding Agent Runtime for the IDE and Beyond}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {220-225}, doi = {10.1145/3837729.3840503}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p47-p (type: Short Paper) doi:10.1145/3837729.3840503

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.
@InProceedings{SPLASH26p226, author = {Zehua Zhang and Jiatong Liu and Xue Yao and Yongqiang Tian}, title = {LPR+: Diverse Transformations for LLM-Aided Program Reduction}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {226-231}, doi = {10.1145/3837729.3840504}, year = {2026}, } Publisher's Version Article: splashcomp26demo-p48-p (type: Short Paper) doi:10.1145/3837729.3840504

Joint SPLASH/ISSTA Posters

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.
@InProceedings{SPLASH26p232, author = {Hadiza Yusuf and Khouloud Gaaloul and Aditi Dharmadhikari}, title = {SiRL: Signal-Level Reinforcement Learning for Falsifying Cyber-Physical Systems}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {232-234}, doi = {10.1145/3837729.3839588}, year = {2026}, } Publisher's Version Article: splashcomp26poster-p3-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839588

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.
@InProceedings{SPLASH26p235, author = {Abdullah Al Noman and Mengfei Ren}, title = {Understanding Correctness Failures in Compiler Optimization}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {235-237}, doi = {10.1145/3837729.3839589}, year = {2026}, } Publisher's Version Article: splashcomp26poster-p4-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839589

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.
@InProceedings{SPLASH26p238, author = {Ruiguo Hu and Dongqi Wang and Shujin Yang and Zhenglin Li and Dongming Chen}, title = {Bridging Call Boundaries: Inter-procedural Semantic Completion for Graph-Based Vulnerability Detection}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {238-240}, doi = {10.1145/3837729.3839590}, year = {2026}, } Publisher's Version Article: splashcomp26poster-p5-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839590

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.
@InProceedings{SPLASH26p241, author = {Haoyi Zhang and Huaijin Ran}, title = {SentryLine: Reviewable Capability Traces for CPython Plugin Hosts}, booktitle = {Proc.\ SPLASH}, publisher = {ACM}, pages = {241-243}, doi = {10.1145/3837729.3839591}, year = {2026}, } Publisher's Version Article: splashcomp26poster-p11-p (type: Extended Abstract (2 pages + 1 page for references only)) doi:10.1145/3837729.3839591

proc time: 1.77