Vladimir Gladshtein
where else to find them
what they talk about
where they keep going back
no series more than once — all 4 in the filters
on a stage with
all 6 in the filters
who talks about the same things
- Qiyuan Zhao5 talks
- Ilya Sergey25 talks
- Oded Padon11 talks
- Samuel Gruetter5 talks
- Adam Chlipala23 talks
- Adithya Murali6 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… | ||
| Hyperreal Specifications for Continuous Sparse Data Computations | Sparse 2025 | 2025-06-16 |
A new relational separation logic called LGTM∞ specifies array-encoded geometric data as code (getter procedures) and generalises hypersafety to real-indexed… | ||
| 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… | ||
| nothing matches | ||