Software verification; Security; Logic and automata theory;
Programming Languages/Formal Methods/Software Engineering Group
Massively Empowered Classrooms (MEC)
, a hybrid MOOC model for Indian undergraduate education, in collaboration with Microsoft Research, India.
Reasoning with heaps/dynamic data structures (Strand and Dryad)
Building reliable software: OS, browsers, etc. with proven security properties
Security of web browser extensions (VEX)
Invariant synthesis using learning
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)
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
Francesco Sorrentino (testing concurrent programs)
Edgar Pek (static analysis; points-to analysis)
Pranav Garg (deductive verification; compositional verification)
Shambwaditya Saha (synthesis)
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
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.
CS498: Logic in Computer Science
CS173: Discrete Structures
CS373: Intro to Theory of Computation
CS477: Formal Methods in Software Development
Also check out the following:
Formal Methods Seminar at Illinois
The new Formal Methods Reading List
PC Member: POPL 2015.
PC Member: PLDI 2014, Edinburgh, Scotland.
PC Member: CONCUR 2014, Rome
PC Member: Highlights of Logic, Automata, Games, Paris
PC Member: CAV 2013, St. Petersburg, Russia
PC Member: MFCS, 2013, IST, Austria
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,
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.