OGAWA, Mizuhito
Professor

School of Information Science, Intelligent Robotics Area, Research Centre for Interpretable AI, Research Center for Theoretical Computer Science

School of Information Science, Intelligent Robotics Area, Research Centre for Interpretable AI, Research Center for Theoretical Computer Science

Ph.D from University Tokyo(2002) 東京大学

: Japan Advanced Institute of Science and Technology (Research Professor, 2003-2007), Japan Advanced Institute of Science and Technology (Professor, 2007-), NII (Visiting Professor, 2008-)

: NTT Electoric Communication Laboratories (researcher, 1985-2001), Japan Science and Technology Corporation (researcher, 2002-2003)

: NTT Electoric Communication Laboratories (researcher, 1985-2001), Japan Science and Technology Corporation (researcher, 2002-2003)

Software

ソフトウェア検証, プログラム解析

**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.

**Confluence of non-left-linear 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., left-linear and nonoverlapping) implies confluence in 1960's and Huet extended it to left-linear and prallel closed TRSs in 1980. For non-left-linear and non-terminating TRSs, Chew showed the unique normal form for strongly nonoverlapping TRSs. Toyama and Oyamaguchi conjectured that strongly nonoverlapping and right-linear 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 BE-PUM 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 VNU-HCMC, we have developped a model generater BE-PUM based on dynamic symbolic execution in an on-the-fly manner. It also works as a robust disassebler, and even as a general unpacker for packed code by many packers.

**Well-structured pushdown systems**

Decidability of infinite state transition systems has been explored in two directions: a well-structured 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 well-quasi ordering equiped for inifnite states. A well-structured pushdown system (WSPDS) combines both still keeping decidability. We showed the decidablity of the coverability if a WSTS has finite control states (and well-quasi-ordered stack alphabet), by using P-automata techniques, which reduced the coverability of a WSPDS into that of a WSTS (P-automaton). 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 quantifier-free constraints. It has many variations of backend theory, e.g. linear arithmetic, uninterpreted function symbols, arrays. They are quite established theories, but non-linear 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 SMT-COMP 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

On Classes of Regular Languages Related to Monotone WQOs.

Mizuhito Ogawa, Victor, L. Selivanov

Descriptional Complexity of Formal Systems - 21st IFIP WG 1.02 International Conference, DCFS 2019, Košice, Slovakia, July 17-19, 2019, Proceedings, 235-247, 2019

Mizuhito Ogawa, Victor, L. Selivanov

Descriptional Complexity of Formal Systems - 21st IFIP WG 1.02 International Conference, DCFS 2019, Košice, Slovakia, July 17-19, 2019, Proceedings, 235-247, 2019

Comparison of Three Deep Learning-based Approaches for IoT Malware Detection.

Khanh Duy Tung, Nguyen, Tran Minh Tuan, Son Hai Le, Viet-Anh Phan, Mizuhito Ogawa, Nguyen Le Minh

10th International Conference on Knowledge and Systems Engineering, KSE 2018, Ho Chi Minh City, Vietnam, November 1-3, 2018, 382-388, 2018

Khanh Duy Tung, Nguyen, Tran Minh Tuan, Son Hai Le, Viet-Anh Phan, Mizuhito Ogawa, Nguyen Le Minh

10th International Conference on Knowledge and Systems Engineering, KSE 2018, Ho Chi Minh City, Vietnam, November 1-3, 2018, 382-388, 2018

Packer identification based on metadata signature

Nguyen Minh Hai, Mizuhito Ogawa, Quan Thanh Tho

ACM International Conference Proceeding Series, -, 2017

Nguyen Minh Hai, Mizuhito Ogawa, Quan Thanh Tho

ACM International Conference Proceeding Series, -, 2017

raSAT: an SMT solver for polynomial constraints

Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa

FORMAL METHODS IN SYSTEM DESIGN, 51, 3, 462-499, 2017

Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa

FORMAL METHODS IN SYSTEM DESIGN, 51, 3, 462-499, 2017

Subtropical satisfiability

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Tung Vu

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10483, 189-206, 2017

Pascal Fontaine, Mizuhito Ogawa, Thomas Sturm, Xuan Tung Vu

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 10483, 189-206, 2017

Generation of Program Analyzer Based on Model Checking

YAMAOKA YUJI, HU ZHENJIANG, TAKEICHI MASATO, OGAWA MIZUHITO

情報処理学会論文誌プログラミング（PRO）, 44, 13, 25-37, 2003

YAMAOKA YUJI, HU ZHENJIANG, TAKEICHI MASATO, OGAWA MIZUHITO

情報処理学会論文誌プログラミング（PRO）, 44, 13, 25-37, 2003

raSAT: SMT for Polynomial Inequality

12th International Workshop on Satisfiability Modulo Theories (SMT2014), TU Wien, Wien Austria, 2014

12th International Workshop on Satisfiability Modulo Theories (SMT2014), TU Wien, Wien Austria, 2014

Non-E-overlapping and weakly shallow TRSs are confluent (Extended abstract)

IWC 2014 (3rd International Workshop on Confluence, TU Wien, Wien Austria, 2014

IWC 2014 (3rd International Workshop on Confluence, TU Wien, Wien Austria, 2014

#### ■Teaching Experience

Formal Languages and Automata(E), Mathematical Logic, Graphs and Automata, Algebra for Computer Scientist, 形式言語とオートマトン(E), 数理論理学, グラフとオートマトン理論, 情報代数

#### ■Contributions to Society

Association for Computing Machinary, IPSJ, JSSST

10th IEEE RIVF International Conference on Computing and Communication Technologies (RIVF-2013) , Thanh-Thuy Nguyen・教授（副学長）・VNU-UET, Vietnam、小川瑞史・教授・JAIST, Japan (PC co-chairs) , 2013 - 2013 , Hanoi, Vietnam http://uet.vnu.edu.vn/rivf2013/

11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013) , Hung Dang-Van・教授・UET-VNU Hanoi, Vietnam、小川瑞史・教授・JAIST, Japan (PC co-chairs) , 2013 - 2013 , Hanoi, Vietnam http://www.uet.vnu.edu.vn/atva2013/index.htmlProceedings appeared as Springer LNCS 8172

11th International Symposium on Automated Technology for Verification and Analysis (ATVA 2013) , Hung Dang-Van・教授・UET-VNU Hanoi, Vietnam、小川瑞史・教授・JAIST, Japan (PC co-chairs) , 2013 - 2013 , Hanoi, Vietnam http://www.uet.vnu.edu.vn/atva2013/index.htmlProceedings appeared as Springer LNCS 8172