On sabbatical, visiting Microsoft Research, India.
Working on a MOOC model for India: check out MEC
Software verification; Security; Logic and automata theory;
Programming Languages/Formal Methods/Software Engineering Group
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)
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)
Xiaokang Qiu (decidable logics for program verification)
Edgar Pek (static analysis; points-to analysis)
Pranav Garg (deductive verification; compositional verification)
Shambwaditya Saha (synthesis)
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.
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 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.
2012: PC Chair: CAV 2012; PC Member: LPAR-18
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.