Steffen Smolka — Staff Software Engineer, Google (original) (raw)
Staff Software Engineer at Google, building the network infrastructure enabling AI at scale. I bring a programming languages andformal methods background to planet-scale systems — delivering tools that enable velocity through reliability, rather than trading one for the other.
Programming Languages AI Infrastructure Network Verification Formal Methods Compilers Tools
01 Overview
At Google, I founded and lead ARCNET (Automated Reasoning and Contracts for Networking) — a team applying formal methods, AI, and domain-specific languages to make Google's data center networks fast and easy to program, evolve, reason about, and get right. Watch this recent talk to get a taste.
I have a theory and research background that I've found surprisingly useful on the applied side. At Cornell, I did a PhD withNate Foster on language-theoretic foundations for network programming and verification — NetKAT, ProbNetKAT, and GKAT — and built compilers and verifiers.
02 Experience
Staff Software Engineer (L6) · Network Infrastructure · Sunnyvale, CA
Founded and leads ARCNET — formal methods and AI for network velocity and reliability at hyperscale.
January 2020 – Present
Engineering Intern · Sunnyvale, CA
June – September 2018
Researched decision procedures for probabilistic programs.
May – September 2017
Intern · Palo Alto, CA
P4 data plane programming and verification — contributed to a data plane verification patent.
September 2016 – February 2017
Designed and implemented a parallelizing compiler for Ziria, a domain-specific language for software-defined radio.
May – August 2015
03 Publications
KATch: A Fast Symbolic Verifier for NetKAT
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
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
Steffen Smolka, Nate Foster, Justin Hsu, Tobias Kappé, Dexter Kozen, and Alexandra Silva.
POPL 20
Proof Carrying Network Code
Christian Skalka, John Ring, David Darais, Minseok Kwon, Sahil Gupta, Kyle Diller, Steffen Smolka, Nate Foster.
CCS 19
Scalable Verification of Probabilistic Networks
Steffen Smolka, Praveen Kumar, David M. Kahn, Nate Foster, Justin Hsu, Dexter Kozen, and Alexandra Silva.
PLDI 19
Performance Annotations for Cloud Computing
HotCloud 17
Cantor Meets Scott: Semantic Foundations for Probabilistic Networks
Steffen Smolka, Praveen Kumar, Nate Foster, Dexter Kozen, and Alexandra Silva.
POPL 17
A Fast Compiler for NetKAT
Steffen Smolka, Spiridon Eliopoulos, Nate Foster, and Arjun Guha.
ICFP 15
Semi-intelligible Isar Proofs from Machine-Generated Proofs
Jasmin Christian Blanchette, Sascha Böhme, Mathias Fleury,Steffen Smolka, and Albert Steckermeier.
JAR 15
Robust, Semi-Intelligible Isabelle Proofs from ATP Proofs
Steffen Smolka and Jasmin Christian Blanchette.
PxTP 13
04 Patents
Cloud Network Reachability Analysis for Virtual Private Clouds
Hui Liu, Leslie Choong, Hongkun Yang, Shishir Agrawal, Raj Yavatkar, Tianqiong Luo, Gargi Adhav, Steffen Smolka.
2024
Data Plane Program Verification
Jeongkeun Lee, Cole Schlesinger, Nate Foster, Han Wang, Robert Soulé, William Hallahan, Steffen Smolka, Mon Jed Liu.
2023
05 Talks
P4-Based Automated Reasoning (P4‑BAR) for the (Networking) Masses!
2024 P4 Workshop · October 2024
Conference presentations from PLDI, POPL, ICFP, and SIGCOMM. Slide decks linked in the publications section above.
06 Selected Honors & Awards
SIGPLAN Distinguished Paper Award
Dec 2019
SIGPLAN Research Highlight
Oct 2016
DAAD Fellowship (Jahresstipendium für Studienaufenthalte im Ausland)
German Academic Exchange Service · ~50 recipients per year across all disciplines in Germany
Nov 2012
Fulbright Fellowship
Declined in favor of DAAD fellowship
Nov 2012
07 Teaching
Teaching Assistant · Adrian Sampson · Cornell University
Spring 2018 PhD
Teaching Assistant · Andrew Myers · Cornell University
Spring 2016 Undergraduate Masters
08 Education
PhD, Computer Science
2013 – 2019
Visiting Student, Computer Science
2016 – 2017
BSc, Computer Science
2010 – 2013