Qiyuan Zhao
where else to find them
no profile links on file
what they talk about
all 4 in the filters
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 8 in the filters
who talks about the same things
- Vladimir Gladshtein5 talks
- Ilya Sergey25 talks
- Oded Padon11 talks
- Zhou Yuanyuan3 talks
- Adam Chlipala23 talks
- Zhong Shao19 talks
| title | conference | date |
|---|---|---|
| Velvet: A Multi-Modal Verifier for Effectful Programs | Dafny 2026 | 2026-01-11 |
Velvet is a Dafny-style verifier implemented as a Lean library that verifies imperative programs with mutable state, loops, and nondeterminism by generating… | ||
| Lessons from Building an Auto-Active Verifier in Lean | Dafny 2026 | 2026-01-11 |
Veil is an auto‑active verifier implemented as a Lean library that does concrete and symbolic model checking, bounded searches, and inductive‑invariant… | ||
| Foundational Multi-Modal Program Verifiers | POPL 2026 | 2026-01-11 |
Paper presents a framework implemented in Lean implementation that provides a library of monad transformers for state, divergence, exceptions and… | ||
| Mechanised Hypersafety Proofs about Structured Data | PLDI 2024 | 2024-06-24 |
Claims a practical verification path: LGTM encodes formats as getter code and proves correctness via parametrised hypersafety triples mechanised as a Coq… | ||
| Rooting for Efficiency: Mechanised Reasoning about Array-Based Trees in Separatio... | CPP 2024 | 2024-01-15 |
Provides a library of definitions, lemmas and proof rules that let one switch between array and tree views (mutually derivable) to localize updates, formalizes… | ||
| nothing matches | ||