Research Interests

  • Software analysis and verification
  • Model checking: algorithms and tools
  • Security
  • Logic and automata theory

    • Current Research

  • Software Analysis:
  • Analysis of heaps in programs using automata
  • Compositional verification using algorithmic learning
  • Synthesizing formal interfaces for software modules using games and learning (JIST)
    •
  • Concurrency:
  • Notions of atomicity for concurrent programs
  • Analyzing concurrent recursive models
    •
  • Security:
  • Preventing script-injection attacks in web applications
    •
  • Automata and logics:
  • Visibly pushdown automata / Automata on nested words
  • Expressive logics and algorithms for models of programs with recursion: Caret, visibly pushdown mu-calculus
  • Model-checking infinite graphs
  • Automata models for XML
    •

    • Courses:

  • Spring '08: CS477: Formal Software Development Methods
  • Fall '07: CS273: Introduction to the Theory of Computation
  • Summer '07 Course in Salerno on Logic, Automata and Algorithms for Graphs
  • Spring '07: Not teaching
  • Fall '06: CS273: Introduction to the Theory of Computation
  • Spring '06: CS498mp: Software Model-Checking
  • Fall '05: CS598mp: Automata and Logic in Verification
  • Spring '05: CS598mp: Algorithmic Software Verification

    • Students:

    I am looking for bright motivated students to work on (a) atomicity and other ways to verify concurrent software, (b) verification of heap-intensive programs, (c) theoretical verification including automata theory, and (d) security for web applications. Contact me by email or drop by my office if you are interested!
  • Azadeh Farzan (co-advised)
  • Gennaro Parlato (visiting)

    • Tutorials

  • Learning Algorithms and Formal Verification
    VMCAI (Verification, Model Checking and Abstract Interpretation) Nice, France.
    (Slides in PDF).

    • Conferences

  • Program Committee: CONCUR 2008 (Int'l Conf on Concurrency Theory), Toronto, Canada.
  • Chairing INFINITY 2007, workshop on infinite state systems, with CONCUR, Lisboa, Portugal.
  • Invited Tutorial: Learning Algorithms and Formal Verification
    VMCAI (Verification, Model Checking and Abstract Interpretation) Nice, France.
  • Invited Talk: Visibly pushdown automata for XML
    EROW (Emerging Research Opportunities in Web Data Management) 2007,
    An ICDT workshop, Barcelona, Spain.
  • Program Committee:
    ICALP 2007 (Int'l Coll. on Automata, Languages, and Programming), Wroclaw, Poland.
    • Earlier:
  • Workshop on Games in Design and Verification; colocated with FLoC (Federated Logic Conference) (which includes CAV, LICS, etc.), Seattle, USA. (Organizer).
  • Invited talk: GALOP'06: Games for Logic and Programming Languages, part of FLoC, Seattle, USA.
  • Workshop on Software Verification; part of FSTTCS 2005, Hyderabad, India (Organizer).
  • PC: ACM 2006 Symposium on Applied Computing: Technical track on software verification, Dijon, France.
  • PC: FSTTCS 2005: Foundations of Software Tech. and Theoretical Comp. Sc., Hyderabad, India.
  • Invited talk: LCC'05: Logic and Computational Complexity, workshop with LICS'05, Chicago.
  • Invited talk: FIT'05: Foundations of Interface Technologies, workshop with CONCUR'05, San Fransisco.
  • PC: CAV 2005: Computer Aided Verification, Edinburgh, UK.
  • PC: GDV 2005: Games in Design and Verification, workshop with CAV 2005, Edinburgh, UK.
  • PC: FORMATS and FTRTFT, 2004
    Joint Conference on Formal Modelling and Analysis of Timed Systems (FORMATS) and Formal Techniques in Real-Time and Fault Tolerant System (FTRTFT).