Research

  1. Certified Program Synthesis with a Multi-modal Verifier

    Yueyang Feng, Dipesh Kafle, Vladimir Gladshtein, Vitaly Kurin, George Pîrlea, Qiyuan Zhao, Peter Müller, and Ilya Sergey

    41st IEEE/ACM International Conference on Automated Software Engineering (ASE 2026). Munich, Germany, October 2026.

    Paper
    BibTeX
    @inproceedings{feng2026certified,
  author    = {Feng, Yueyang and Kafle, Dipesh and Gladshtein, Vladimir and
               Kurin, Vitaly and P{\^i}rlea, George and Zhao, Qiyuan and
               M{\"u}ller, Peter and Sergey, Ilya},
  title     = {Certified Program Synthesis with a Multi-modal Verifier},
  booktitle = {Proceedings of the 41st IEEE/ACM International Conference on
               Automated Software Engineering (ASE '26)},
  address   = {Munich, Germany},
  numpages  = {13},
  month     = oct,
  year      = {2026},
  publisher = {ACM}
}

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

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

    38th International Conference on Computer Aided Verification (CAV 2026). Lisbon, Portugal, July 2026. LNCS 16683, pages 228–242.

    PaperDOICode
    BibTeX
    @inproceedings{gladshtein2026velvet,
  author    = {Gladshtein, Vladimir and Kurin, Vitaly and Feng, Yueyang and
               Kafle, Dipesh and P{\^i}rlea, George and Zhao, Qiyuan and
               Sergey, Ilya},
  title     = {Velvet: A Foundational Multi-Modal Verifier for Imperative
               Programs in Lean},
  booktitle = {CAV},
  series    = {Lecture Notes in Computer Science},
  volume    = {16683},
  pages     = {228--242},
  year      = {2026},
  publisher = {Springer},
  doi       = {10.1007/978-3-032-32526-6\_11}
}

  3. Multi-Modal Program Verification in Velvet

    Ilya Sergey

    Proofs and Intuitions. Tutorial, 21 January 2026.

    Read

  4. 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. PACMPL 10(POPL), Article 77.

    PaperDOICode
    BibTeX
    @article{gladshtein2026foundational,
  author    = {Gladshtein, Vladimir and P{\^i}rlea, George and Zhao, Qiyuan and
               Kurin, Vitaly and Sergey, Ilya},
  title     = {Foundational Multi-Modal Program Verifiers},
  journal   = {Proc. ACM Program. Lang.},
  volume    = {10},
  number    = {POPL},
  articleno = {77},
  numpages  = {32},
  month     = jan,
  year      = {2026},
  publisher = {ACM},
  doi       = {10.1145/3776719}
}

  5. Velvet: A Multi-Modal Verifier for Effectful Programs

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

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

    Paper
    BibTeX
    @inproceedings{gladshtein2026velvetdafny,
  author    = {Gladshtein, Vladimir and P{\^i}rlea, George and Zhao, Qiyuan and
               Kurin, Vitaly and Sergey, Ilya},
  title     = {Velvet: A Multi-Modal Verifier for Effectful Programs},
  booktitle = {Dafny Workshop (Dafny'26)},
  address   = {Rennes, France},
  month     = jan,
  year      = {2026}
}