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.

Talks

You can check out recordings of some of my past talks in this YouTube playlist.

News & Updates

Guarded Kleene Algebra with Tests received a SIGPLAN Distinguished Paper Award.	Dec '19
Our paper on Guarded Kleene Algebra with Tests has been accepted to POPL 2020!	Sep '19
Our paper Proof Carrying Network Code has been accepted to CCS 2019!	Sep '19
I will attend the Bellairs workshop on Network Verification in Barbados in March 2020.	Sep '19
I serve on the External Review Committee for PLDI 2020.	Aug '19
I passed my PhD defense!	Aug '19
A recording of my PLDI talk on Scalable Verification of Probabilistic Networks is now online.	Aug '19
Check out our latest preprint on Guarded Kleene Algebra with Tests!	Jul '19
The slides from my PLDI talk on Scalable Verification of Probabilistic Networks are now online.	Jun '19
I gave a talk on Scalable Verification of Probabilistic Networks at the Workshop on Foundations of Routing in Ithaca, NY.	Jun '19
Check out the video abstract (plus bonus) for our upcoming PLDI paper.	Jun '19
Camera-ready of "Scalable Verification of Probabilistic Networks" (PLDI'19) shipped.	Apr '19
Our paper Scalable Verification of Probabilistic Networks was (conditionally) accepted at PLDI 19!	Feb '19
I will attend the Bellairs workshop on Learning and Verification in Barbados in March!	Feb '19
I'm excited to spend the summer in the Bay Area to work on Google Cloud!	April '18
I gave a talk on Probabilistic Network Verification at the Data Communication & Cloud Network Forum in Santa Clara, CA.	Mar '18
I gave a talk on Probabilistic Network Verification at the Shonan meeting Theory and Practice of Data Plane Programming in Japan.	Feb '18
We presented a poster about our work on program equivalence for ProbNetKAT at PPS 2018. Also see this short blog entry.	Jan '18
I'm excited to work with Alexandra Silva at UCL in London over the summer!	Jun '17
I will give a NetKAT tutorial on Tuesday (April 18, 2017). It will be live streamed on YouTube.	Apr '17
I'm excited to attend the Bellairs workshop on Probabilistic Programming Languages in Barbados.	Mar '17
The slides for our POPL'17 paper Cantor Meets Scott are now online.	Jan '17
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!	Oct '16
I am visiting Stanford until February. I am also working part time at Barefoot Networks.	Sep '16
I gave a 5-minute talk on A Domain-Theoretic Foundation for Probabilistic NetKAT at Lake Placid.	Jul '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.	Jun '16
I discussed current work on probabilistic NetKAT at NEPLS.	May '16
Attending IFIP Working Group 2.8 meeting at Lake Placid	July '16
I'm attending the Bellairs Workshop on Formal Methods for Software-Defined Networks in Barbados.	Mar '16
I'm attending the 2nd P4 Workshop at Stanford.	Nov '15
I presented our work on A Fast Compiler for NetKAT at ICFP 2015 in Vancouver (see a video here).	Sep '15
I'm attending SIGCOMM 2015 in London.	Aug '15
We just shipped the camera-ready version of A Fast Compiler for NetKAT, to appear at ICFP'15.	Jun '15
I am excited to work with with Dimitrios Vytiniotis at Microsoft Research in Cambridge over the summer.	Jun '15
I serve on the Artifact Evaluation Committee for PLDI 2015.	Feb '15
I'm attending POPL 2015 in Mumbai.	Jan '15

Projects (current & past)

• 
• 
• Ziria: A DSL for wireless systems programming
• 

Publications

KATch: A Fast Symbolic Verifier for NetKAT [ paper | code ] Mark Moeller, Jules Jacobs, Olivier Savary Bélanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, Alexandra Silva.	PLDI 24
SwitchV: Automated SDN Switch Validation with P4 Models [ conference paper | talk ] Kinan Dak Albab, Jonathan Dilorenzo, Stefan Heule, Ali Kheradmand, Steffen Smolka, Konstantin Weitz, Muhammad Tirmazi, Jiaqi Gao, Minlan Yu.	SIGCOMM 22
Guarded Kleene Algebra with Tests: Verification of Uninterpreted Programs in Nearly Linear Time [ conference paper | full paper ] Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva.	POPL 20
Proof Carrying Network Code [ paper ] Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffen Smolka, Nate Foster.	CCS 19
Scalable Verification of Probabilistic Networks [ conference paper | full paper | slides | video | another video | skit | code ] Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva.	PLDI 19
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 | code ] 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

Theses

A (Co)algebraic Approach to Programming and Verifying Computer Networks [ thesis ] Steffen Smolka. PhD Thesis in Computer Science. Cornell University. December 2019.

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

Teaching

Guest lecturer, CS 6114: Network Programming Languages, Nate Foster, Cornell University, Fall 2018.

Guest lecturer, CS 6861: Introduction to Kleene Algebra, Dexter Kozen, Cornell University, Spring 2018.

Guest lecturer, CS 3110: Data Structures and Functional Programming, Nate Foster, Cornell University, Spring 2018.

Teaching assistant, CS 6110: Advanced Programming Languages, Adrian Sampson, Cornell University, Spring 2018.

Guest lecturer, CS 6114: Network Programming Languages, Nate Foster, Cornell University, Fall 2017.

Teaching assistant, CS 4120/5120: Compilers, Andrew Myers, Cornell University, Spring 2016.

Teaching assistant, Introduction to Computer Science 2, Andrey Rybalchenko, TU München, Fall 2011.

Industry Experience

Google, Engineering Intern, Sunnyvale CA, June - September 2018.

Barefoot Networks, Intern, Palo Alto CA, September 2016 - February 2017.

Microsoft Research, Research Intern, Cambridge UK, May - August 2015.

Service

Programming Language Design and Implementation (PLDI), External Review Committee, 2020.

Symposium on Networked Systems Design and Implementatio (NSDI), Reviewer, 2018.

Transactions on Programming Languages and Systems (TOPLAS), Reviewer, 2018.

Journal of Logical and Algebraic Methods in Programming, Reviewer, 2017.

Principles of Programming Languages (POPL), Artifact Evaluation Committee, 2016.

Programming Language Design and Implementation (PLDI), Artifact Evaluation Committee, 2015.