Zhong Shao
where else to find them
what they talk about
all 4 in the filters
where they keep going back
- POPL5 editions2022–2025
- OOPSLA4 editions2020–2024
- PLDI Workshop Honoring Andreas Podelski3 editions2024–2026
all 4 in the filters
on a stage with
all 28 in the filters
who talks about the same things
- Yuting Wang5 talks
- Jérémie Koenig4 talks
- Ling Zhang4 talks
- Ji-Yong Shin6 talks
- Longfei Qiu5 talks
- Arthur Oliveira Vale3 talks
| title | conference | date |
|---|---|---|
| SureDistrib: Verifying Almost-Sure Termination of Composite Asynchronous Byzantine(…) | PLDI 2026 | 2026-06-15 |
SureDistrib defines probabilistic IO automata in the Rocq proof assistant and proves composition lemmas that let an abstract underlay be replaced by an… | ||
| LiDO-DAG: A Framework for Verifying Safety and Liveness of DAG-Based Consensus Protocols | PLDI 2025 | 2025-06-16 |
LiDO-DAG gives an abstract concurrent-object model and a refinement proof showing DAG protocols simulate leader-based consensus, implemented in Coq and… | ||
| CompCertOC: Verified Compositional Compilation of Multi-threaded Programs with Shared(…) | PLDI 2025 | 2025-06-16 |
Claim: a verified compiler that compositionally preserves semantics for cooperative multi-threaded C programs that share stack data. Key techniques are… | ||
| Unifying compositional verification and certified compilation with a three-dimensional(…) | POPL 2025 | 2025-01-19 |
A concrete claim: a three-dimensional algebra of refinement composes module interfaces, abstraction levels, and state views so compiler correctness, linking… | ||
| AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects | OOPSLA 2024 | 2024-10-20 |
Claims a single abstraction, AdoB abstraction, unifies benign and Byzantine consensus and lets proofs be done by refinement; implements it in Coq with… | ||
| Compositionality and Observational Refinement for Linearizability with Crashes | OOPSLA 2024 | 2024-10-20 |
Defines a compositional model for full-system crashes and proves that a new criterion, crash-aware linearizability, supports both locality and observational… | ||
| LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs | PLDI 2024 | 2024-06-24 |
LiDO is a refinement-ready model that adds an explicit pacemaker state so liveness of partially synchronous Byzantine SMR reduces to a few safety invariants… | ||
| Compositional Development of Certified System Software | GALOP 2024 | 2024-01-14 |
Claims a new semantics that makes horizontal and vertical composition of linearizable concurrent objects workable, replacing ad hoc inlining with a categorical… | ||
| Fully Composable and Adequate Verified Compilation with Direct Refinements betwe... | POPL 2024 | 2024-01-14 |
Claims a Kripke Memory Relation (called NGP) that is transitive and absorbs per-pass rely/guarantee conditions so a single direct refinement relates Clight… | ||
| A Compositional Theory of Linearizability | POPL 2023 | 2023-01-15 |
Presents a concrete reformulation of linearizability derived from a base concurrent model via the Karoubi envelope, producing a compositional model by… | ||
| Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Tem | OOPSLA 2022 | 2022-12-05 |
Claims a formally verified real-time OS kernel that enforces budget-enforcing EDF partitions and proves temporal isolation between partitions under the… | ||
| Proof Assistants for PL and Math | POPL 2022 Virtual Workshop | 2022-01-27 |
Panel reports active, practical work: large libraries (Lean + mathlib, ~700k LOC) and successful formalizations (including the four‑color style project and… | ||
| Verified Compilation of C Programs with a Nominal Memory Model | POPL 2022 | 2022-01-16 |
The paper claims a drop-in generalization of CompCert’s block memory model into a nominal memory model that uses atoms/supports to rename and separate blocks… | ||
| Layered and Object-Based Game Semantics | POPL 2022 | 2022-01-16 |
Presents a concrete game-semantics model where a layer interface is an object type plus an object strategy, implementations are regular maps from underlay to… | ||
| Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent D | OOPSLA 2021 | 2021-10-17 |
Presents a fault-aware ADO model that exposes partial failures (uncommitted but visible updates) while hiding protocol internals, and a verification stack… | ||
| CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files | OOPSLA 2020 | 2020-11-15 |
CompCertELF is a Coq-verified C-to-ELF toolchain that adds a verified assembler and supports verified separate compilation by proving commutativity between… | ||
| nothing matches | ||