Steven S. Lyubomirsky

sslyu (at)

I am a second-year graduate student at the University of Washington's Programming Languages and Software Engineering group. My (informal) adviser is Zachary Tatlock. I am interested in program verification, both verification of existing programs and systems after the fact with proof assistants or solver-aided tools and developing tools and frameworks to make it easier to write programs with proven correctness properties.

I presently work on the Bagpipe project, for verifying BGP configurations. An offshoot of the Bagpipe project is the SpaceSearch library, allowing for reasoning about the reduction of a problem to SMT in Coq and then extracting the proof of correctness to a solver-aided tool in Rosette.


Konstantin Weitz, Steven Lyubomirsky, Stefan Heule, Emina Torlak, Michael D. Ernst, and Zachary Tatlock. 2017. SpaceSearch: a library for building and verifying solver-aided tools. Proc. ACM Program. Lang. 1, ICFP, Article 25 (August 2017), 28 pages. DOI: