Publications

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.