Ali Kheradmand
2107 Siebel Center for Computer Science
University of Illinois at Urbana-Champaign
201 N. Goodwin ave, Urbana, IL 61801
[my_surname[:7]2@illinois.edu] [LinkedIn] [Google Scholar] [GitHub]
I am was a PhD student in the Department of Computer Science at the University of Illinois at Urbana-Champaign, advised by professors Brighten Godfrey and Grigore Rosu. I am broadly interested in topics at the intersection of theoretical and practical aspects of computer science. My research is currently focused on enhancing the reliability of systems and networks through automated reasoning. It spans areas including formal methods and programming languages as well as computer networks and distributed systems. My more recent works also span AI/ML and inductive program synthesis.
UPDATE: I'm now at Google working with the Network Infrastructure group.
Education
University of Illinois at Urbana-Champaign, Urbana, IL
PhD in Computer Science (2014 - 2021)
Dissertation: Foundations for Practical Network Verification (pdf)
Sharif University of Technology, Tehran, Iran
BSc in Computer Engineering (2010-2014)
Experiences
Google, Sunnyvale, CA
Software Engineer, Fall 2021 - present
Veriflow Inc. (Acquired by VMware), Champaign, IL
Software Engineer - Intern, Summer 2018 - Fall 2019
Fujitsu Laboratories of America, Sunnyvale, CA
Research Intern, Summer 2016, Summer 2017, Fall 2017
University of Illinois at Urbana-Champaign, Urbana, IL
Research Assistant, 2014 - 2021
Ecole Polytechnique Federale de Lausanne (EPFL), Lausanne, Switzerland
Research Intern, Summer 2013
Publications
SwitchV: Automated SDN Switch Validation with P4 Models, SIGCOMM'22 (pdf)
with Kinan Dak Albab, Jonathan DiLorenzo, Stefan Heule, Steffen Smolka, Konstantin Weitz, Muhammad Timarzi, Jiaqi Gao, Minlan Yu
A Framework for Mining High-Level Intents from Low-Level Network Behavior, draft (pdf, NetVerify'21 presentation, code)
with Brighten Godfrey
Towards Verified Self-Driving Infrastructure, HotNets'20 (pdf, slides, presentation, code)
with Bingzhe Liu, Matthew Caesar, Brighten Godfrey
Automatic Inference of High-Level Network Intents by Mining Forwarding Patterns, SOSR'20 (pdf, slides, presentation, code)
with especial thanks to Brighten Godfrey
Plankton: Scalable Network Configuration Verification through Model Checking, NSDI'20 (pdf, slides)
with Santhosh Prabhu, Kuan-Yen Chou, Brighten Godfrey, Matthew Caesar
A Precise and Expressive Lattice-theoretical Framework for Efficient Network Verification, ICNP'19 (pdf, tech report, slides)
with Alex Horn, Mukul R. Prasad
P4K: A Formal Semantics of P4 and Applications, arXiv'18 (pdf, slides, code)
with Grigore Rosu
Predicting Network Futures with Plankton, APNet'17 (pdf, slides)
with Santhosh Prabhu, Brighten Godfrey, Matthew Caesar
Delta-net: Real-time Network Verification Using Atoms, NSDI'17 (pdf, slides, dataset)
with Alex Horn, Mukul R. Prasad
Lockout: Efficient Testing for Deadlock Bugs, WoDet'14 (pdf, slides, code)
with Baris Kasikci, George Candea
US Patent 11,184,282 B1, Packet Forwarding in a Network Device, Nov. 21, 2021 (pdf)
with Santhosh Prabhu
US Patent 10,574,582 B2, Network Property Verification, Feb. 25, 2020 (pdf)
with Alex Horn
US Patent 10,439,926 B2, Network Analysis, Oct. 8, 2019 (pdf)
with Alex Horn
US Patent 10,305,776 B2, Network Verification, May 28, 2019 (pdf)
with Alex Horn
US Patent 10,057,166 B2, Network Verification, Aug. 21, 2018 (pdf)
with Alex Horn, Mukul R. Prasad