Context-sensitive models for multi-thread programs

时间：2012-06-08 分类：学术报告

Title: Context-sensitive models for multi-thread programs
Speaker: Prof. Mizuhito Ogawa (JAIST)
Time: 14:00, Thursday, June 14th, 2012
Venue: Room 337, 3rd Floor, Building 5#, State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences
Abstract: We briefly overview the recent results on models of multi-thread Boolean valued programs. For multi-thread programs, viewpoints of classification consist of (1) context sensitivity, (2) dynamic thread creation, and (3) synchronization. The target property is decidability of reachability. There are classical results that 2-stack pushdown systems are Turing complete, and both context and synchronization sensitivity lead undecidability.

We investigate decidability with certain restrictions, e.g.,
– constraints on push/pop (e.g., context bounded, scope bounded)
– thread creation under no synchronization, and
– locking protocols (e.g., nesting, bounded lock chain, contextual)

We conclude with our recent collaboration with Dr. Xiaojuan Cai (SJTU).

Bio:
Mizuhito Ogawa received his M.S. (mathematics) in 1985 and Ph.D degree (computer science) in 2002, both from University of Tokyo. He worked in NTT Laboratories from 1985 until 2001, and in JST from 2002 to 2003. From 2003, he has been working at School of Information Science, Japan Advanced Institute of Science and Technology (JAIST) as a professor. He has been also a visiting professor at National Institute of Informatics (NII) since 2008.

His research interest focuses on formal methods from theory to practical algorithms and its proto-type implementation. Theory includes term rewriting systems (e.g., confluence), formal languages (e.g., models of multi-thread programs), mathematical logic (e.g., theorem provers and program extraction), and combinatorics (e.g., ordering structures and graphs). Proto-type implementation covers scalable context-sensitive program analyses based on weighted pushdown model checking, SMT for polynomial constraints, and formal proofs of combinatorics.