* Corresponding author; † Equal contribution.
|
EBFuzz: Breaking Hidden Structural Assumptions in Compilers via Extended Assembly Injection ContributionEBFuzz is a novel compiler testing technique that exploits GNU C extended inline assembly to systematically construct legal yet structurally unusual programs via control-flow edge injection and data-flow perturbation.
|
|
Validating Optimizing SMT Solvers via Cross-Theory Approximation ContributionIRis implements the cross-theory approximation methodology to validate optimizing SMT solvers by exploiting relationships between solution spaces of different logical theories, uncovering 24 previously unknown bugs in Z3 and OptiMathSAT (20 subsequently fixed by developers).
|
|
Beyond Coverage: Automatic Test Suite Augmentation for Enhanced Effectiveness Using Large Language Models ContributionSUNG and RAGTIME form a fully automatic LLM-based pipeline for test suite augmentation: SUNG generates semantic-level mutants for mutation testing, and RAGTIME generates test cases targeting the survived mutants, raising mutation scores by 16.04% (standalone) and 8.11% (non-standalone methods) while reducing false positives in LLM-based code generation evaluation.
|
|
Towards Understanding the Bugs in Verilator, a Hardware Description Language Compiler ContributionThis empirical study systematically characterizes the bugs in Verilator, a widely used hardware description language compiler, offering insights that guide future testing and debugging of HDL compilers.
|
|
Using a Sledgehammer to Crack a Nut? Revisiting Automated Compiler Fault Isolation ContributionThis study contributes to a deeper understanding of practical compiler fault localization by demonstrating that the simple, developer-aligned BIC-based (BASIC) strategy significantly outperforms conventional Spectrum-Based Fault Localization (SBFL) techniques.
|
|
Once4All: Skeleton-Guided SMT Solver Fuzzing with LLM-Synthesized Generators ContributionOnce4All is a novel LLM-assisted fuzzing framework for SMT solvers that synthesizes reusable term generators from documentation to efficiently ensure syntactic validity and semantic diversity, dramatically reducing computational overhead and latency.
|
|
Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation ContributionAries is a novel validation technique that thoroughly explores the SMT solver's rewrite space by using mimetic mutation and deductive rewriting to identify critical bugs, particularly in the rewrite systems.
|
|
Unveiling Compiler Faults via Attribute-Guided Compilation Space Exploration ContributionATLAS is a novel attribute-guided compiler testing approach that strategically inserts C/C++ attributes into test programs, enabling a more flexible and comprehensive exploration of the compilation space to uncover bugs in compilers like GCC and LLVM.
|
|
Debugger Toolchain Validation via Cross-Level Debugging ContributionDevil is a novel debugger toolchain validation framework that introduces Cross-Level Debugging (CLD) to compare execution traces from the same executable at different debugging levels, overcoming limitations of prior approaches by establishing robust consistency relations.
|
* Corresponding author; † Equal contribution.