Research Interests

Software verification; Security; 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.

Current research Projects

My current research interests are primarily in software verification 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 interest in program synthesis also centers around using learning algorithms to synthesize program expressions from various kinds of specification.
  • 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)
  • 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
  • Synthesis for network design
  • Building reliable software: OS, browsers, etc. with proven security properties (ASPLOS 2013), proving properties of cloud systems.
  • 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)

    Software/tools:

  • 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:

    Post-doctoral researchers::
  • Daniel Neider (automated deductiver verification, synthesis, learning, invariant synthesis)
    Post-doctoral researcher in the ExCAPE project, jointly at Illinois and UCLA.
  • 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

  • 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

  • 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. sample problems