I have completed my PhD and am now at Google working in Dan Lenoski's Network Infrastructure group.
Steffen Smolka
PhD [ thesis ]
Department of Computer Science
Cornell University
Adviser: Nate Foster
Office: 442 Gates Hall
Email: [first].[last]@gmail.com
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.
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)
Publications
KATch: A Fast Symbolic Verifier for NetKAT
[ paper | code ]
|
PLDI 24 |
SwitchV:
Automated SDN Switch Validation with P4 Models
[ conference paper | talk ]
|
SIGCOMM 22 |
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 | another 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. |