
Mizuhito Ogawa Professor
School of Information Science¡¢Intelligent Robotics Area
¢£Degrees
Ph.D from University Tokyo(2002)
¢£Professional Career
NTT Electoric Communication Laboratories (researcher, 19852001), Japan Science and Technology Corporation (researcher, 20022003), Japan Advanced Institute of Science and Technology (Research Professor, 20032007), 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, nonlinear term rewriting systems, decidability issues in formal languages.
¢£Research Keywords
verification, analysis, theorem proving, model checking, combinatorics, rewriting, formal language.
¢£Research Interests
Contextsensitive analyses for Largescale Java programs The aim of the research is to design and implement various contexsensitive analyses of largescale Java programs (say, 10000 methods) based on weighted pushdown model checking. The main focus is a contextsensitive and flow insensitive pointsto 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. Confluence of nonleftlinear term rewriting systems Confluence ans termination are basic properties of term rewriting systems (TRSs). When termination holds, Knuth and Bendix showed in 1970s that local confluence of critical pairs is enough for confluence. For nonterminationg TRSs, Rosen showed the orthogonality (i.e., leftlinear and nonoverlapping) implies confluence in 1960's and Huet extended it to leftlinear and prallel closed TRSs in 1980. For nonleftlinear and nonterminating TRSs, Chew showed the unique normal form for strongly nonoverlapping TRSs. Toyama and Oyamaguchi conjectured that strongly nonoverlapping and rightlinear TRSs are confluent in 1990, which is still an open problem. Many attempts based on decreasing diagrams failed so far, and we are tackling with a new proof techniques, called reduction graphs. Our current resutl is, a strongly nonoverlapping and weakly shallow TRS is confluent Binary code analyzer BEPUM for malware Program analysis consists of two steps: model generation and model checking. For high level programming languages, such as C, Java, mthe former is straight forward by generating a contol flow graph (CFG). However, binary code, especially malware, it is not easy, since it does not distinguish code and data, and there are lots of obfuscation techniques, e.g., self modification and indirect jump. With the collaboration with VNUHCMC, we have developped a model generater BEPUM based on dynamic symbolic execution in an onthefly manner. It also works as a robust disassebler, and even as a general unpacker for packed code by many packers. Wellstructured pushdown systems Decidability of infinite state transition systems has been explored in two directions: a wellstructured transition system (WSTS), e.g., petri net, proposed by Finkl, et.al. on 1987, and a pushdown system, which has a stack. The key is a wellquasi ordering equiped for inifnite states. A wellstructured pushdown system (WSPDS) combines both still keeping decidability. We showed the decidablity of the coverability if a WSTS has finite control states (and wellquasiordered stack alphabet), by using Pautomata techniques, which reduced the coverability of a WSPDS into that of a WSTS (Pautomaton). Our techniques cover many existing decidability resutls, e.g., braching VAS, recursive VASS, alternating VASS, multiset PDS. We also applied to variations of timed pushdown systems, nested timed automata (NeTA) with frozen clocks. A NeTA has finitely many timed automata as its control states and its stack alphabet. We showed the decidability of its reachability if it has at most one global clock. raSAT: SMT solver for nonlinear constraints An SMT solver solves the satisfiability of quantifierfree constraints. It has many variations of backend theory, e.g. linear arithmetic, uninterpreted function symbols, arrays. They are quite established theories, but nonlinear artihmetic (polynomials) are still under investigation. The ultimate method is based on computer algebra, however, it does not scale. We take an alternative apractical approach based on interval arithmetic and the intermediate value theorem. Our idea is implemented as the tool raSAT, which has participated the internation SMT solver competition SMTCOMP 2015. It obtained 3rd among 6 tools in QFNRA category (nonlinear constraint over reals) and 2nd among 7 tools in QFNIA category (nonlinear constraint over integers). raSAT: SMT solver for nonlinear constraints An SMT solver solves the satisfiability of quantifierfree constraints. It has many variations of backend theory, e.g. linear arithmetic, uninterpreted function symbols, arrays. They are quite established theories, but nonlinear artihmetic (polynomials) are still under investigation. The ultimate method is based on computer algebra, however, it does not scale. We take an alternative apractical approach based on interval arithmetic and the intermediate value theorem. Our idea is implemented as the tool raSAT, which has participated the internation SMT solver competition SMTCOMP 2015. It obtained 3rd among 6 tools in QFNRA category (nonlinear constraint over reals) and 2nd among 7 tools in QFNIA category (nonlinear constraint over integers).
¢£Publications
¡þPublished Papers
 A SlidingWindow Algorithm for OnTheFly Interprocedural Program Analysis¡¤Xin Li, Mizuhito Ogawa¡¤19th International Conference on Formal Engineering Methods,ICFEM17¡¤Springer LNCS
 raSAT : An SMT Solver for Polynomial Constraints Formal Methods in System Design, Springer,¡¤Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa¡¤Formal Methods in System Design, Springer¡¤Available online¡¤2017/06/27
 Subtropical Satisfiability¡¤Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Tung Vu¡¤FroCos 2017¡¤Springer LNCS 10483
Display All
¡þLectures and Presentations
 NonEoverlapping and weakly shallow TRSs are confluent (Extended abstract)¡¤Masahiko Sakai, Michio Oyamaguchi and Mizuhito Ogawa¡¤IWC 2014 (3rd International Workshop on Confluence¡¤TU Wien, Wien Austria¡¤2014713
 raSAT: SMT for Polynomial Inequality¡¤To Van Khanh, Vu Xuan Tung and Mizuhito Ogawa¡¤12th International Workshop on Satisfiability Modulo Theories (SMT2014)¡¤TU Wien, Wien Austria¡¤2014718
¢£Extramural Activities
¡þAcademic Society Affiliations
 Information Processing Society in Japan, SIGPRO¡¤2007
 IPSJ SIGPRO¡¤Editorial board member¡¤2006
 JSSST¡¤Editorial board member¡¤20052008
Display All
