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 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.

Presently I am part of the SAML project, which is an interdisciplinary research group holistically exploring problems spanning the machine learning stack. My involvement concerns investigating ways to apply techniques from programming languages in the development and deployment of machine learning systems.

I have previously worked 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.


Conference Papers

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:

Workshop Papers

Jared Roesch, Steven Lyubomirsky, Logan Weber, Joshua Pollock, Marisa Kirisame, Tianqi Chen, and Zachary Tatlock. Relay: A New IR for Machine Learning Frameworks. Proceedings of the 2nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL 2018). To appear June 2018.

Background vector created by GarryKillian -