Publications

1. Foundational Multi-Modal Program Verifiers

   Vladimir Gladshtein, George Pîrlea, Qiyuan Zhao, Vitaly Kurin, and Ilya Sergey

   53rd ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2026). Rennes, France, January 2026.

   Paper Code

2. Lessons from Building an Auto-Active Verifier in Lean

   George Pîrlea, Vladimir Gladshtein, Qiyuan Zhao, and Ilya Sergey

   Dafny Workshop 2026 (co-located with POPL 2026). Rennes, France, January 2026.

   Paper

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

   George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey

   37th International Conference on Computer Aided Verification (CAV 2025). Zagreb, Croatia, July 2025.

   Paper Code Artefact