Ali Kheradmand

2107 Siebel Center for Computer Science

University of Illinois at Urbana-Champaign

201 N. Goodwin ave, Urbana, IL 61801

[my_surname[:7]] [LinkedIn] [Google Scholar] [GitHub]

I am 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 analysis and verification, spanning areas including formal methods, programming languages, and automated software engineering as well as computer networks and distributed systems.


  • University of Illinois at Urbana-Champaign, Urbana, IL

    • PhD (in progress) in Computer Science (2014 - present)

  • Sharif University of Technology, Tehran, Iran

    • BSc in Computer Engineering (2010-2014)


  • 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

  • Ecole Polytechnique Federale de Lausanne (EPFL), Lausanne, Switzerland

    • Research Intern, Summer 2013


  • 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 Probhu, 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 Probhu, 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 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

  • JP Patent Application 2018-046549 A, Network Verification, March 22, 2018 (pdf)

    • with Alex Horn, Mukul R. Prasad