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

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. (A recording will follow soon.)
Oct 16 Cantor meets Scott at POPL 2017 in Paris. See you there!
Oct 16 Our paper A Fast Compiler for NetKAT was recognized as a SIGPLAN Research Highlight!
Sep 16 I am visiting Stanford until February. I am also working part time at Barefoot Networks.
Jul 16 I gave a 5-minute talk on A Domain-Theoretic Foundation for Probabilistic NetKAT at Lake Placid.
Jun 16 I serve on the Artifact Evaluation Committee for POPL 2017.
Jun 16 I gave a talk on efficent language abstractions for SDN at the Network Programming Retreat in NYC.
May 16 I discussed current work on probabilistic NetKAT at NEPLS.
Mar 16 I'm attending the Bellairs Workshop on Formal Methods for Software-Defined Networks in Barbados.
Jun 15 I am excited to work with with Dimitrios Vytiniotis at Microsoft Research in Cambridge over the summer.

Projects (current & past)


Deciding Probabilistic Program Equivalence in NetKAT technical report | extended abstract | poster ]
Steffen Smolka, David Kahn, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva.
PPS 18
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.