Research Interests

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

    • Research Projects

  • Model-checking abstractions of programs
  • Testing concurrent programs
  • Annotation and proof mechanisms for safe concurrency
  • Finding security vulnerabilities in web browser extensions
  • Decidable logics for heaps
  • Synthesizing programs

    • Current Research: Click here

    Courses:

  • Spring '10: CS373: Introduction to Theory of Computation
  • Spring '09: CS373: Introduction to Theory of Computation
  • Fall '08: CS498: Logic in Computer Science
  • 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:

    Current:

  • Sruthi Bandhakavi (security; security of web extensions)
  • Francesco Sorrentino (testing concurrent programs)
  • Xiaokang Qiu (decidable logics for program verification)
  • Rajesh Karmani
  • Edgar Pek

    • Former students advised:

  • Azadeh Farzan -- now part of the faculty at Univ. of Toronto
    •  Prospective students: I am always looking for students who want to work on verification of software.
    I look for students who can combine theory and practice--- if you don't want to implement at all, or if you are interested only in implementing systems and not in theory, you should probably look at other groups.
    Contact me by email or drop by my office if you are interested!

    Post-doctoral researchers:

  • Gennaro Parlato

    • Conferences

  • Program Committee: FSTTCS 2010: Foundations of Software Tech. and Theoretical Comp. Sc., Chennai, India.
  • Program Committee: 8th Int'l Symposium on Automated Technology for Verification and Analysis (ATVA), Singapore, 2010.
  • Program Committee: 27th Symposium on Theoretical Aspects of Computer Science (STACS), Nancy, France, 2010.
  • Dagstuhl Workshop on Design and Validation of Concurrent Systems, Dagstuhl, Germany, Aug 30, 2009.
  • Program Committee: 21st Int'l Conf on Computer Aided Verification (CAV 2009), Grenoble, France.
  • Program Committee: 24th Annual IEEE Symposium on Logic in Computer Science (LICS 2009), Los Angeles, USA.
  • Program Committee: 16th International Symposium on Temporal Representation and Reasoning (TIME 2009), Brixen-Bressanone, Italy.
  • External Review Committee: ACM SIGPLAN 2009 Conference on Programming Language Design and Implementation (PLDI 2009), Dublin, Ireland.
    • Earlier:
  • Co-organizer: Workshop on Security and Reliability in Software Systems, with FSTTCS, Bangalore, India, 2008.
  • Program Committee: Sixth ASIAN Symposium on Programming Languages and Systems (APLAS), Bangalore, India, 2008.
  • 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.
    (Slides in PDF).
  • 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.
  • 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).