Mizuhito Ogawa Professor
School of Information Science（Department of Information Science・Software Science）

■Degrees

Ph.D from University Tokyo(2002)

■Professional Career

NTT Electoric Communication Laboratories (researcher, 1985-2001), Japan Science and Technology Corporation (researcher, 2002-2003), Japan Advanced Institute of Science and Technology (Research Professor, 2003-2007), Japan Advanced Institute of Science and Technology (Professor, 2007-), NII (Visiting Professor, 2008-)

■Specialties

The main theme is formal verication, from theory to application. Main methodology is theorem proving and model checking, applied to program anayses and security protocol verifications. Theoretical research covers efficient algorithms based on combinatorics, non-linear term rewriting systems, decidability issues in formal languages.

■Research Keywords

verification, analysis, theorem proving, model checking, combinatorics, rewriting, formal language.

■Research Interests

Context-sensitive analyses for Large-scale Java programs
The aim of the research is to design and implement various contex-sensitive analyses of large-scale Java programs (say, 10000 methods) based on weighted pushdown model checking. The main focus is a context-sensitive and flow insensitive points-to analysis, and we proposed a new algorithm based on weighted pushdown model checking. Its implementation is ongoing with SOOT (translation to an intermediate language Jimple) as a frontend anf Weighted PDS library as a backend analysis engine.

■Publications

■Extramural Activities