Research Interests

Software verification; Security; Program Synthesis and Machine Learning; Logic and automata theory;
Programming Languages/Formal Methods/Software Engineering Group

Outreach Interests

Massively Empowered Classrooms (MEC), a hybrid MOOC model for Indian undergraduate education, in collaboration with Microsoft Research, India.

Note to prospective students

I am actively looking for Ph.D. students in the following areas. If you are interested, please apply for the Ph.D. program and write to me personally.
  • Machine learning and program synthesis; learning logics
  • Building verified software using almost-automated verification, especially distributed systems like blockchain and bitcoin
  • Logics for program verification: especially logis amenable to automated reasoning for expressive logics for heap manipulation.
  • Sound and mostly complete automation for logics using natural proofs.
  • Current research Projects

    My current research interests are primarily in software verification and synergies between machine learning and program synthesis. The main approach that I currently believe in for automating software verification are centered aroud the synergy of two techniques: natural proofs for solving logical reasoning required in verification and learning-based techniques to synthesize invariants required for inductively proving programs correct. My interests also lie in bringing together program synthesis and machine learning--- I believe practical pattern matching inductive techniques can be combined with deductive logics to build more intelligent systems.
  • Natural proofs: sound techniques for undecidable problems in verification.
  • Natural proofs for reasoning with data-structures and dynamic heaps (see Dryad and VCDryad) (POPL 2012, PLDI 2013, PLDI 2014, and completeness results in POPL 2017)
  • Natural proofs for correctness of distributed systems (OOPSLA 2014)
  • Invariant Generation, especially using machine learning (CAV 2013, SAS 2013, CAV 2014, POPL 2016).

  • Synthesis (NSF ExCAPE Expeditions)
  • Synthesis using learning (TACAS 2016)
  • Synthesis for network design (SOSR 2015)
  • Building reliable software: building a verified blockchain distributed system. Earlier: building OS, browsers, etc. with proven security properties (ASPLOS 2013).
  • Earlier research Projects

  • Decidable logics for reasoning with heaps/dynamic data structures (Strand)
  • Security of web browser extensions (VEX)
  • Testing concurrent programs (Penelope)
  • Security of access control (VAC)
  • Annotation and proof mechanisms for safe concurrency (Accord)
  • Model-checking abstractions of programs (Getafix)
  • Decidable automata models (See page on visibly pushdown automata)


  • VCDryad - An extension of VCC that provides sound but incomplete automatic mechanisms against Dryad specifications, a dialect of separation logic.
  • Dryad - Sound but incomplete mechanism for proving heap-based programs correct
  • CAV 2013 tool - for learning universally quantified invariants on linear data-structures using quantified data automata
  • Strand - Decidable logics/SMT solver for reasoning with heaps
  • Getafix - A boolean model-checker for concurrent and recursive programs
  • VEX - Static analysis of web-browser extensions for security vulnerabilities
  • Penelope - A testing tool for concurrent programs
  • VAC - Verifier of Access Control
  • JIST - Java Interface Synthesis Tool

  • Students and Post-doctoral researchers:

    Students currently advised:
  • Francesco Sorrentino (testing concurrent programs)
  • Edgar Pek (static analysis; points-to analysis)
  • Pranav Garg (deductive verification; compositional verification)
  • Shambwaditya Saha (synthesis)
  • Formerly advised:
  • Students:
  • Xiaokang Qiu
    Thesis: Automatic Techniques for Proving Correctness of Heap-Manipulating Programs
    Now postdoc at MIT/UMD.
  • Sruthi Bandhakavi; security of web extensions -- now at Google
  • Postdocs:
  • Gennaro Parlato -- now faculty at University of Southampton
  • Karl Palmskog-- now a postdoc at UT Austin.
  • Daniel Neider (automated deductiver verification, synthesis, learning, invariant synthesis)
    Post-doctoral researcher in the ExCAPE project, jointly at Illinois and UCLA. -- now at Max Planck Institute

  • Courses:

    Note to graduate students: If you are interested in mainstream software verification, I suggest that you take the course CS477 (Formal Methods in Software Development) followed by my course CS598MP (offered only once in a while) on Software Verification. The CS598MP course is more advanced, and CS477 will be a pre-requisite for it in the future. I also strongly encourage you to take the CS498 course on "Logic in Computer Science" (aka Logical Systems) offered by me or Prof. Viswanathan before you take CS58MP:Software Verification.
  • Spring '14: CS498: Logic in Computer Science
  • Fall '13: CS173: Discrete Structures
  • Fall '11: CS373: Intro to Theory of Computation
  • Spring '11: CS477: Formal Methods in Software Development
  • Earlier courses
  • Also check out the following:
  • Formal Methods Seminar at Illinois
  • The new Formal Methods Reading List

  • Service

  • PC Member: POPL 2019
  • PC Member: CONCUR 2018
  • PC Member: Workshop on Automated Deduction for Separation Logics (ADSL), affiliated with LICS and FLOC, 2018.
  • PC Member: TACAS 2017
  • PC Member: Highlights of Logic, Automata, and Games, 2017.
  • PC Member: International Conference on Runtime Verification (RV 2017).
  • Tutorial on Machine-learning based methods for synthesizing invariants. , at Computer Aided Verification (CAV), San Fransisco, USA, 2015.
  • PC Member: ICALP 2016: Int'l Colloq. on Automata Languages and Programming, Rome, Italy.
  • External Review Committee: CAV 2016: Computer Aided Verification, Toronto, Canada.
  • Co-chair/Organizer: SYNT 2015: 4th Workshop on Synthesis (associated CAV), San Francisco, USA.
  • PC Member: Trustworthy Global Computing (TGC), 2015, Madrid, Spain.
  • ERC Member: PLDI 2015, Portland, Oregon, USA.
  • PC Member: ACM/IEEE International Conference on Model Driven Engineering Languages and Systems, 2014, Madrid, Spain.
  • PC Member: POPL 2015, Mumbai, India.
  • PC Member: PLDI 2014, Edinburgh, Scotland.
  • PC Member: CONCUR 2014, Rome, Italy
  • PC Member: SAS 2014, Munich, Germany
  • Earlier
  • 2013: PC Member: MFCS, 2013, CAV 2013, Highlights of Logic, Automata, Games
  • 2012: PC Chair: CAV 2012; PC Member: LPAR-18, POPL 2012.
  • 2011: PC Member: CAV 2011, ATVA 2011, FSTTCS 2011.
  • 2010: PC Member: FSTTCS 2010, ATVA 2010, STACS 2010,
  • 2009: PC member: CAV 2009, LICS 2009, TIME 2009; Ext Rev Committee: PLDI 2009
  • 2008: PC Member: APLAS 2008, CONCUR 2008.
  • 2007 PC Chair: INFINITY 2007 (with CONCUR); PC Member: ICALP 2007
  • 2006 PC member: ACM SAC.
  • 2005 PC member: FSTTCS 2005, CAV 2005. GDV 2005 (with CAV'05).
  • 2004 PC member: FORMATS and FTRTFT, 2004
  • Other Activities: Organized events, invited talks, etc.