Research Interests

Software verification; Security; Logic and automata theory

Research Projects   [Click here for more on current research]

  • Building reliable software: OS, browsers, etc.
  • Security of web browser extensions (VEX)
  • Decidable logics for heaps (Strand and Dryad)
  • Testing concurrent programs (Penelope)
  • Security of access control (VAC)
  • Annotation and proof mechanisms for safe concurrency (Accord)
  • Model-checking abstractions of programs (Getafix)
  • Compositional verification
  • Static points-to analysis
  • Synthesizing programs
  • Decidable automata models (See page on visibly pushdown automata)

    • Software/tools:

  • Strand - Decidable logics/SMT solver for reasoning with heaps
  • Dryad - Sound but incomplete mechanism for proving heap-based programs correct
  • 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:

    Currently advising:
  • Sruthi Bandhakavi (security; security of web extensions)
  • Francesco Sorrentino (testing concurrent programs)
  • Xiaokang Qiu (decidable logics for program verification)
  • Edgar Pek (static analysis; points-to analysis)
  • Pranav Garg (deductive verification; compositional verification)
    •  Other students I work with currently:
  • Rajesh Karmani (annotation languages for safe concurrency)
  • Vijay Korthikanthi (program synthesis)
    •  Formerly advised:
  • Students: Azadeh Farzan -- now part of the faculty at Univ. of Toronto
  • Postdocs: Gennaro Parlato

    • 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.
  • 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 Chair: CAV 2012, Berkeley, USA.
         24th Int'l Conference on Computer Aided Verification.
  • PC Member: LPAR 2012, Merida, Venezuela.
         18th Int'l Conf on Logic for Programming, Artifical intelligence, and Reasoning
  • PC Member: POPL 2012, Philadelphia, USA.
          ACM SIGACT-SIGPLAN Symp. on Principles of Programming Languages.
    • Earlier
  • 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.