Word cloud created using http://www.wordle.net/ using titles of recent publications

## Research:

**
****My research agenda is to build techniques and tools for
verifying the correctness of software programs and, in that process,
find bugs.
**

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:

**Applications:**
Verification of control-intensive properties of device drivers and
other systems code.

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
atomicity.

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)
Synthesizing programs
**Techniques:**
Static analysis, abstract interpretation
Predicate abstraction
Hoare-style deductive verification for concurrent programs
Model-checking (explicit, BDD-based, SAT-based).
Dynamic analysis
Automata-theoretic model-checking
Compositional verification (using learning)
Algorithmic Learning
**Theory**:
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
Algorithms
Decidable theories and MSO; combinations of decision procedures