Deprecated: The each() function is deprecated. This message will be suppressed on further calls in /home/zhenxiangba/zhenxiangba.com/public_html/phproxy-improved-master/index.php on line 456
Madhusudan's page
[go: Go Back, main page]

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:
  • Member of UPCRC
    (MS-Intel supported research team to make parallel programming easy)
  • 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:
    Click to see webpage on VPAs/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:

  • 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
  • Francesco Sorrentino

    • Former students advised:

  • Azadeh Farzan -- now part of the faculty at Univ. of Toronto
    •  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!

    Post-doctoral researchers:

  • Gennaro Parlato

    • Tutorials

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

    • Conferences

  • 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.
  • Dagstuhl Workshop on Design and Validation of Concurrent Systems, Dagstuhl, Germany, Aug 30, 2009.
  • 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 , Bangalore, India.
  • Program Committee: CONCUR 2008 (Int'l Conf on Concurrency Theory), Toronto, Canada.
    • Earlier:
  • 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.
  • 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).