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