Zhendong Su
where else to find them
what they talk about
all 11 in the filters
where they keep going back
- OOPSLA5 editions2020–2025
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
all 8 in the filters
on a stage with
all 51 in the filters
who talks about the same things
- Shaohua Li5 talks
- Yu Jiang21 talks
- Thodoris Sotiropoulos5 talks
- Chengyu Zhang5 talks
- Quan Zhang4 talks
- Chijin Zhou5 talks
| title | conference | date |
|---|---|---|
| Neuro-Symbolic Proof Generation for Scaling Systems Software Verification | 20th USENIX Symposium on Operating Systems Design and Implementation (OSDI '26) | 2026-07-13 |
Neuro-symbolic proof search implements a best-first tree search that repeatedly queries a fine-tuned LLM for single-step tactics, executes each step in a new… | ||
| Semantic Reification: A New Paradigm for Random Program Generation | PLDI 2026 | 2026-06-15 |
Claims a new semantic reification method that synthesizes a program P, input I, and expected output O from a CFG skeleton and a chosen execution path… | ||
| An Empirical Study of Bugs in the rustc Compiler | OOPSLA 2025 | 2025-10-16 |
Analysis of 301 rustc issues from 2022–2024 shows concrete fault patterns: about 30% root in the type system, ~15% in ownership, ~15% from MIR optimizations… | ||
| Divergence-Aware Testing of Graphics Shader Compiler Back-Ends | PLDI 2025 | 2025-06-16 |
ShaDiv generates shader tests that deliberately perturb control and data flow divergence to exercise backend optimizations, uses a divergence-aware generator… | ||
| Relaxing Alias Analysis: Exploring the Unexplored Space | PLDI 2025 | 2025-06-16 |
This study instruments LLVM 17.0.6 and SPEC CPU 2017 and shows that removing alias analysis entirely changes final binaries only slightly on average, but only… | ||
| The Hidden Program State Hurts Everyone | Onward! 2024 | 2024-10-23 |
Argues that hidden program state slows developers, demonstrates a graph-based live-state language called Algot (also written Alot in studies) that lets users… | ||
| When Your Infrastructure is a Buggy Program: Understanding Faults in Infrastructure as(…) | OOPSLA 2024 | 2024-10-20 |
360 bugs across Ansible Puppet Chef registries are analyzed and classified into six symptom groups (most commonly external configuration failures), ten root… | ||
| Validating SMT Solvers for Correctness and Performance via Grammar-based Enumeration | OOPSLA 2024 | 2024-10-20 |
ET is a grammar-based enumerator that compiles eight SMT theory grammars into algebraic datatypes and drives the FEAT enumerator to produce smallest-to-largest… | ||
| SMT2Test: From SMT Formulas to Effective Test Cases | OOPSLA 2024 | 2024-10-20 |
SMT2Test transforms SMT formulas into executable programs (Dafny and C via an intermediate representation) and encodes satisfiability as a reachability… | ||
| Understanding and Finding Java Decompiler Bugs | OOPSLA 2024 | 2024-10-20 |
Systematic study of 333 real bug reports identifies that 40.2% have small repro tests, over 80% manifest as exceptions, syntactic, or semantic errors, and the… | ||
| Validating the eBPF Verifier via State Embedding | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
State embedding validates the eBPF verifier by taking concrete runtime states from profiling and folding, encoding them into an eBPF program so the verifier… | ||
| Detecting Logic Bugs in Database Engines via Equivalent Expression Transformation | 18th USENIX Symposium on Operating Systems Design and Implementation (OSDI '24) | 2024-07-10 |
Proposes equivalent expression transformation that rewrites expressions (using CASE-based rewrites and boolean identities) so semantics stay the same while… | ||
| Boosting Compiler Testing by Injecting Real-World Code | PLDI 2024 | 2024-06-24 |
Tool Creal injects real-world functions into Csmith-generated seeds, extracting 50,000 functions from 100+ popular GitHub projects, inferring input/output… | ||
| Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior | PLDI 2024 | 2024-06-24 |
Automated pipeline instruments C programs generated by cith with runtime checks, then injects compiler builtins (unreachable/assume) to encode observed dead… | ||
| API-driven Program Synthesis for Testing Static Typing Implementations | POPL 2024 | 2024-01-14 |
Thalia synthesizes small, type‑intensive client programs from real libraries by building an API graph and enumerating typing sequences that drive… | ||
| Accelerating Fuzzing through Prefix-Guided Execution | OOPSLA 2023 | 2023-10-23 |
Introduces prefix-guided execution that monitors a test's partial run (a sequence of basic block IDs) and applies early termination when the prefix is already… | ||
| Detecting Transactional Bugs in Database Engines via Graph-Based Oracle Construction | OSDI 2023 | 2023-07-10 |
A tool called TxCheck builds statement-dependency graphs via SQL-level instrumentation and uses transactional oracle construction to generate semantically… | ||
| Generative Type-Aware Mutation for Testing SMT Solvers | OOPSLA 2021 | 2021-10-17 |
Generative Type-Aware Mutation implements expression mutation using SMT-LIB operator signatures to produce grammatically correct but larger mutants, realized… | ||
| Fully Automated Functional Fuzzing of Android Apps for Detecting Non-Crashing Logic Bugs | OOPSLA 2021 | 2021-10-17 |
Proposes independent view fuzzing and a tool called Genie that automatically mines a GUI transitional model, finds independent event traces, injects them into… | ||
| SANRAZOR: Reducing Redundant Sanitizer Checks in C/C++ Programs | 15th USENIX Symposium on Operating Systems Design and Implementation (OSDI '21) | 2021-07-14 |
SanRazor is a tool that identifies and removes redundant sanitizer checks by combining dynamic coverage profiles with static data-dependency trees, instruments… | ||
| Finding Bugs in Database Systems via Query Partitioning | OOPSLA 2020 | 2020-11-15 |
Automated testing partitions a query into three cases — ϕ, NOT ϕ, and ϕ IS NULL — then recomposes them (using UNION ALL) and compares results; implemented as… | ||
| Fast Linear Programming through Transprecision Computing on Small and Sparse Data | OOPSLA 2020 | 2020-11-15 |
Analyzes ~500,000 simplex tableaux from Polly PPCG and HayStack and finds >99% of coefficients <9 bits, medians of 18 columns and 84% sparsity, with rare… | ||
| On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers | OOPSLA 2020 | 2020-11-15 |
Proposes type-aware operator mutation: randomly replace operators with others of the same SMT-LIB type, chain mutations, and cross-check Z3 vs CVC4 to spot… | ||
| nothing matches | ||