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

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.
June '16 I serve on the Artifact Evaluation Committee for POPL 2017.
June '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.
June '15 I am excited to work with with Dimitrios Vytiniotis at Microsoft Research in Cambridge over the summer.

Projects (current & past)

Publications

Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
conference version | full paper | slides ]
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva.
POPL 17
A Fast Compiler for NetKAT paper | slides | video | code | award ]
Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha
ICFP 15
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

Teaching

CS 4120/5120: Compilers, Cornell University, Spring 2016
Introduction to Computer Science 2, Technische Universität München, Fall 2011