


Steffen Smolka
PhD
Department of Computer Science
Cornell University
Adviser: Nate Foster
Office: 442 Gates Hall
Email: [lastname]@cs.cornell.edu
Google Scholar
Github
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
Sep '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 Probabilistic Programming in Barbados in March 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. |
Jul '19 | Check out our latest preprint on Guarded Kleene Algebra with Tests! |
Jun '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. |
Apr '19 | Camera-ready of "Scalable Verification of Probabilistic Networks" (PLDI'19) shipped. |
Feb '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! |
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 Verification at the Data Communication & Cloud Network Forum in Santa Clara, CA. |
Feb '18 | I gave a talk on Probabilistic Network Verification at the Shonan meeting Theory and Practice 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! |
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. |
July '16 | Attending IFIP Working Group 2.8 meeting at Lake Placid |
Mar '16 | I'm attending the Bellairs Workshop on Formal Methods for Software-Defined Networks in Barbados. |
Nov '15 | I'm attending the 2nd P4 Workshop at Stanford. |
Sep '15 | I presented our work on A Fast Compiler for NetKAT at ICFP 2015 in Vancouver (see a video here). |
Aug '15 | I'm attending SIGCOMM 2015 in London. |
Jun '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. |
Feb '15 | I serve on the Artifact Evaluation Committee for PLDI 2015. |
Jan '15 | I'm attending POPL 2015 in Mumbai. |
Projects (current & past)
Publications
Guarded Kleene Algebra with Tests:
Verification of Uninterpreted Programs in Nearly Linear Time
[ conference paper | full paper ]
|
POPL 20 |
Proof Carrying Network Code
[ paper ]
|
CCS 19 |
Scalable Verification of Probabilistic Networks
[ conference paper | full paper | slides | video | skit | code ] |
PLDI 19 |
Performance Annotations for Cloud Computing
[ paper ]
|
HotCloud 17 |
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
[ conference version | full paper | technical notes | slides | code ] |
POPL 17 |
A Fast Compiler for NetKAT
[ paper | slides | video | code | award ]
|
ICFP 15 |
Semi-intelligible Isar Proofs from Machine-Generated Proofs
[ paper ]
|
JAR 15 |
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
[ paper | slides ]
|
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, , Cornell University, Fall 2018. |
Guest lecturer, CS 6861: Introduction to Kleene Algebra, , Cornell University, Spring 2018. |
Guest lecturer, CS 3110: Data Structures and Functional Programming, , Cornell University, Spring 2018. |
Teaching assistant, CS 6110: Advanced Programming Languages, , Cornell University, Spring 2018. |
Guest lecturer, CS 6114: Network Programming Languages, , Cornell University, Fall 2017. |
Teaching assistant, CS 4120/5120: Compilers, , Cornell University, Spring 2016. |
Teaching assistant, Introduction to Computer Science 2, , 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. |