Steven S. Lyubomirsky

sslyu (at)

I am a third-year Ph.D. 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 SAMPL, which is an interdisciplinary research group holistically exploring problems spanning the machine learning stack. I am specifically working on the Relay project, whose purpose is to enable new abstractions and optimizations in machine-learning frameworks by providing an expressive intermediate representation and new compilation pipeline for TVM.

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, Josh Pollock, Marisa Kirisame, Tianqi Chen, and Zachary Tatlock. 2018. Relay: a new IR for machine learning frameworks. In Proceedings of the 2nd ACM SIGPLAN International Workshop on Machine Learning and Programming Languages (MAPL 2018). ACM, New York, NY, USA, 58-68. DOI:

Background vector created by GarryKillian -