Research Overview

I enjoy working on problems at the intersection of theory and practice. My interests include language design, (probabilisitc) semantics, compilers, automata theory, formal verification, and algorithms.

I am passionately working on making networks more programmable.

Before coming to Cornell, I received a B.Sc. in Computer Science from Technische Universität München, where I worked with Jasmin Blanchette on the interactive theorem prover Isabelle.

Recent News & Talks

April 18 I'm excited to spend the summer in the Bay Area to work on Google Cloud!
Mar 18 I gave a talk on Probabilistic Network Verificiation at Huawei's Data Communication & Cloud Network Forum in Santa Clara, CA.
Feb 18 I gave a talk on Probabilistic Network Verificiation at the Shonan meeting Theory and Practise of Data Plane Programming in Japan.
Jan 18 We presented a poster about our work on program equivalence for ProbNetKAT at PPS 2018. Also see this short blog entry.
Jun 17 I'm excited to work with Alexandra Silva at UCL in London over the summer!
Apr 17 I will give a NetKAT tutorial on Tuesday (April 18, 2017). It will be live streamed on YouTube.
Mar 17 I'm excited to attend the Bellairs workshop on Probabilistic Programming Languages in Barbados.
Jan 17 The slides for our POPL'17 paper Cantor Meets Scott are now online.
Oct 16 Cantor meets Scott at POPL 2017 in Paris. See you there!

Projects (current & past)


Probabilistic Program Equivalence for NetKAT draft ]
Steffen Smolka, Praveen Kumar, Nate Foster, Justin Hsu, David Kahn, Dexter Kozen, and Alexandra Silva.
Performance Annotations for Cloud Computing paper ]
Daniele Rogora, Steffen Smolka, Antonio Carzaniga, Amer Diwan, and Robert Soulé.
HotCloud 17
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
conference version | full paper | technical notes | slides ]
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva.
A Fast Compiler for NetKAT paper | slides | video | code | award ]
Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha.
Semi-intelligible Isar Proofs from Machine-Generated Proofs paper ]
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury, Steffen Smolka, and Albert Steckermeier.
JAR 15
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs paper | slides ]
Steffen Smolka and Jasmin Christian Blanchette.
PxTP 13


Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs thesis | slides ]
Steffen Smolka. Bachelor Thesis in Computer Science. Technische Universität München. August 2013.


CS 6110: Advanced Programming Languages, Adrian Sampson, Cornell University, Spring 2018.
CS 4120/5120: Compilers, Andrew Myers, Cornell University, Spring 2016.
Introduction to Computer Science 2, Andrey Rybalchenko, Technische Universität München, Fall 2011.