Word cloud created using http://www.wordle.net/ using titles of recent publications
My research agenda is to build techniques and tools for
verifying the correctness of software programs and, in that process,
Verification of control-intensive properties of device drivers and
other systems code.
My research philosophy is to work on the border between
theory and practice--- to consider well-motivated problems in verification,
explore and solve the underlying problem using theoretical analysis
(involving logic, algorithms, and automata theory), and apply these
to build real and practical solutions.
My current research interests:
See Getafix: A Boolean program checker for
model-checking sequential and concurrent Boolean abstractions of programs.
Verification of concurrent programs, in particular race-freedom and
Member of Microsoft-Intel funded center UPCRC.
Verification of heap-based properties of programs.
Security of web browser extensions, in particular detection of
security vulnerabilities in Firefox extensions.
Security of access contol policies
Mining specifications from code (see JIST, a Java Interface Synthesis Tool)
Static analysis, abstract interpretation
Hoare-style deductive verification for concurrent programs
Model-checking (explicit, BDD-based, SAT-based).
Compositional verification (using learning)
Logics for specifying control-flow properties, especially in
recursive programs (e.g. CaRet)
Decidable logics for heap analysis
Hoare logic style verification of concurrent programs
Automata theory: decidable automata on infinite graphs
Visibly pushdown automata and recursion
See the Visibly pushdown automata / Nested Words page
Decidable theories and MSO; combinations of decision procedures