Publications

2026

Velvet: A Foundational Multi-Modal Verifier for Imperative Programs in Lean

Vladimir Gladshtein, Vitaly Kurin, Yueyang Feng, Dipesh Kafle, George Pîrlea, Qiyuan Zhao, Ilya Sergey. CAV 2026.

Formalization of a Realistic Verification-Condition Generator for an Intermediate Verification Language

Vladimir Gladshtein, K. Rustan M. Leino. ITP 2026.

Lazy Proof Automation for Separation Logic

Valentin Mikhalchuk, Vladimir Gladshtein, Ilya Sergey. ITP 2026.

Foundational Multi-Modal Program Verifiers

Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey. POPL 2026.

Velvet: A Multi-Modal Verifier for Effectful Programs

Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, Ilya Sergey. Dafny Workshop 2026.

Lessons from Building an Auto-Active Verifier in Lean

George Pîrlea, Vladimir Gladshtein, Qiyuan Zhao, Ilya Sergey. Dafny Workshop 2026.

Veil: A Framework for Automated and Interactive Verification of Transition Systems

George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, Ilya Sergey. CAV 2025.

Mechanised Hypersafety Proofs about Structured Data

Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, Ilya Sergey. PLDI 2024.

Small Scale Reflection for the Working Lean User

Vladimir Gladshtein, George Pîrlea, Ilya Sergey. In submission, 2024.

Truly Stateless, Optimal Dynamic Partial Order Reduction

Michalis Kokologiannakis, Iason Marmanis, Vladimir Gladstein, Viktor Vafeiadis. POPL 2022.

Mechanized Theory of Event Structures: A Case of Parallel Register Machine

Vladimir Gladstein, Dmitry Mikhailovsky, Evgenii Moiseenko, Anton Trunov. SYRCOSE 2021.