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, 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