Qinxiang Cao
where else to find them
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 5 in the filters
on a stage with
- Xiwei Wu2×
- Andrew W. Appelonce
- Di Wangonce
all 16 in the filters
who talks about the same things
- Zhong Shao19 talks
- Hongfei Fu6 talks
- Qinlin Chen3 talks
- Thomas Reps20 talks
- David Sanan4 talks
- Zhe Hou2 talks
| title | conference | date |
|---|---|---|
| Denotation-based Compositional Compiler Verification | PLDI 2026 | 2026-06-15 |
Proposes a denotational framework that represents each statement by three behavior sets (normal, error, divergence) enriched with traces and distinguishes… | ||
| Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic | OOPSLA 2025 | 2025-10-16 |
Claims a mechanical reduction of ∀∃ relational Hoare triples to ordinary unary Hoare triples by redefining relational validity and internalizing the ∀∃ pattern… | ||
| VEP: A Two-stage Verification Toolchain for Full eBPF Programmability | NSDI '25 | 2025-04-28 |
VEP is a two-stage verifier: VEP-C (annotation-guided C verifier), a VEP-compiler that preserves annotations through compilation, and VEP-eBPF, a lightweight… | ||
| VST-A: A Foundationally Sound Annotation Verifier | POPL 2024 | 2024-01-14 |
VST-A is an annotation verifier that parses C into control‑flow graphs, splits functions into paths (four paths for the linked‑list reverse example) and… | ||
| Interactive Theorem Proving in Logic Education：A Coq Formalization of ZFC Set T... | CoqPL 2023 | 2023-01-21 |
A Coq deep embedding of ZFC and a textbook-style deduction system plus a small automation layer produce a mini ZFC prover that hides Coq internals and exposes… | ||
| nothing matches | ||