EXPRESS 2026 – Preliminary Table of Contents

CoVerif: An Automated Contract Verifier for Java using Symbolic Execution
Aryan Kumar, Alex Toppo, and Sandip Ghosal
(Birla Institute of Technology, Mesra, India)
Specifying contracts as program behavior using Hoare triples is an established practice in software engineering. Compared to traditional testing approaches, formal verification of these contracts provides stronger guarantees of functional correctness. However, its practical adoption has remained limited since significant effort required to develop verification harnesses for individual modules. In this paper, we present CoVerif, a symbolic verification engine designed to address this gap. Given a Java class and a set of program contracts, CoVerif automatically generates the necessary verification infrastructure to perform exhaustive symbolic execution using Symbolic PathFinder (SPF). We evaluate our proposed tool on 12 Java classes that include two linear and five non-linear data structures, and five library wrappers, covering more than 120 contracts. The evaluation demonstrates that CoVerif successfully verifies the implementations and identifies all injected faults, including a bug in a third-party library wrapper. These results demonstrate the potential of CoVerif to facilitate wider industrial adoption for verifying API-level functionality.

Article Search Article: splashws26expressmain-p18-p (type: Short Paper (4 pages, excluding references and appendices)) doi:10.1145/3842650.3843173

Vulnerability Trends across Open-Source AI-Attributed Code
Clarisa Caballero-Ignacio, Lucas Stephens, Josiah Sage, Manish Motwani, and Zane Ma
(Oregon State University, USA)
Recent advances in large language models (LLMs) have led to widespread adoption of AI-coding tools and increasing deployment of AI-assisted code. While AI’s potential for programming productivity is becoming evident, the security of AI-attributed code is still poorly understood. In this work, we collect the largest set of in-the-wild AI-attributed code to date, examining 253,390 files containing AI-assisted code from seven tools and 9,544 human-written files from public GitHub repositories. Our analyses reveal significant differences in security-relevant CWE prevalence across programming languages and AI tools, with tool-specific differences varying by language. Additionally, human-written Python exhibited significantly higher security-relevant CWE prevalence than AI-attributed Python (21.08% vs. 11.15%) with higher CVSS severity. Ultimately, our results extend prior work showing that vulnerable AI-assisted code is making it into public repositories, indicating a need for stronger review practices and greater developer security awareness when using these tools.

Article Search Article: splashws26expressmain-p25-p (type: Full Paper (8 pages, excluding references and appendices)) doi:10.1145/3842650.3843174

Towards Budget-Aware Early Candidate Selection for Vulnerability Analysis
Xinye Zhao and Joanna Cecilia da Silva Santos
(University of Notre Dame, USA)
Actionable warning identification (AWI) prioritizes static-analysis warnings under limited review budgets, but most work ranks final warnings or complete source-to-sink paths. These artifacts are expensive to produce and are typically unavailable early in a vulnerability-analysis pipeline. We study budget-aware early candidate selection from lightweight candidates, including suspicious sinks, source–sink fragments, and vulnerability-looking methods. We define budget as the percentage of candidates that downstream validation can inspect and compare heuristic, learned, and diversity-aware ranking policies. On CWE-Bench-Java, diversity-aware random-forest ranking recovers 62.5% of oracle-covered vulnerable samples at a 10% candidate budget, compared with 29.1% for random selection. On OWASP Benchmark Java and Semgrep-derived OWASP candidates, ranking also improves low-budget sample discovery under case-level proxy labels. These results suggest that early candidate ranking can better allocate limited validation effort, while future work should connect this stage to concrete downstream validation costs.

Article Search Article: splashws26expressmain-p67-p (type: Short Paper (4 pages, excluding references and appendices)) doi:10.1145/3842650.3843175

Decomposing LLM-Based Testing with Agent Skills: A Case Study on Numerical Inconsistencies
Yutong Wang and Cindy Rubio-González
(University of California at Davis, USA)
LLM-based testing can expose subtle reliability issues in numerical software, but monolithic prompts make it hard to inspect which guidance drives effectiveness. We study whether Agent Skills can make such workflows more explainable by factoring procedural knowledge into composable testing components. Using numerical inconsistency detection as a case study, we decompose an LLM-based differential-testing pipeline into Skills for program generation and feedback-guided mutation, then evaluate four Skill configurations. Our results show that the feedback-guided mutation Skill setting yields the largest improvement on inconsistency rate (+12 percentage points), while enriching Skills with additional procedural knowledge slightly decreases performance (−3 percentage points). An exploratory evaluation with agent-native execution reveals scalability challenges for high-iteration Skill workflows.

Article Search Article: splashws26expressmain-p75-p (type: Short Paper (4 pages, excluding references and appendices)) doi:10.1145/3842650.3843176

How Faithfully Do LLMs Implement Mutated Specifications? An Empirical Study of Grammar-Guided Protocol Testing
Polina Kozyreva and Endadul Hoque
(Syracuse University, USA)
Testing implementations of binary protocols for specification compliance requires inputs that satisfy both structural and semantic constraints. Purely random generation and primitive mutations are often insufficient for exploring semantically meaningful behaviors in protocols that rely on Type-Length-Value (TLV) encoding, yet domain-specific compliance testing tools require deep protocol expertise and significant manual effort to construct. This work investigates whether grammar-level mutation combined with LLM-based code synthesis can serve as a viable, more generalizable approach to specification compliance testing.
We evaluate the approach on PKCS#1 v1.5 signature verification–a widely deployed TLV-encoded standard with a formally verified testing oracle (Morpheus)–across 48 cryptographic library implementations. We reproduced 10 of 13 non-trivial specification violation categories previously identified by Morpheus, including all 5 signature forgery categories, and discovered 1 previously unreported discrepancy. We found that LLM hallucination–occurring in 82.5% of generated scripts–is the primary factor limiting effectiveness, not the mutation strategies. We identify five distinct hallucination types and show that their distribution varies systematically across mutation categories: structural mutations are implemented with 13.3% fidelity while constraint mutations achieve 30.3% correctness but suffer the highest rate of mutations being fully ignored (8.1%). These findings reveal a striking gap between operational reliability (99.8%) and semantic fidelity (17.5%), providing actionable guidance on when LLM-based code synthesis can be trusted in specification-driven testing pipelines.

Article Search Article: splashws26expressmain-p91-p (type: Full Paper (8 pages, excluding references and appendices)) doi:10.1145/3842650.3843177

EXPRESS 2026 – Preliminary Table of Contents

2nd Workshop on Explainable and Reliable Software Systems (EXPRESS 2026)

Frontmatter

2nd Workshop on Explainable and Reliable Software Systems (EXPRESS 2026) Papers

2nd Workshop on Explainable and Reliable Software Systems (EXPRESS 2026)