* Corresponding author; † Equal contribution.
|
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).
|
|
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.