Vladimir Gladshtein
Vladimir Gladshtein

✉ vovaglad at u.nus.edu

✉ vova at lean-fro.org

📍 School of Computing, NUS COM1, 13 Computing Drive, Singapore 117417

I am a PhD student at the National University of Singapore, advised by Ilya Sergey. I am also a member of LeanFRO where I am building tools for reasoning about monadic Lean code.

My research focuses on building scalable, trustworthy verification frameworks. I have contributed to

  • Velvet, a Dafny-style multi-modal verifier

  • Loom, a library for reasoning about monadic Lean programs

  • Veil, a framework for distributed protocol verification

  • B3, an SMT-based intermediate verification language, successor of Boogie

Important fact

In general, people tend to use Vlad as a shortened version of my name. However, that is incorrect). If you want to use accurate short forms for my name, they would be:

  • Vova (Most common)

  • Volodya (Most formal)

  • Mira (Most unusual)

  • Vovan (Most informal)