Transforming Termination by Self-Labelling. - Aart Middeldorp; Hitoshi Ohsaki; Hans Zantema (CADE, 1996)

Equational Termination by Semantic Labelling. - Hitoshi Ohsaki; Aart Middeldorp; Jürgen Giesl (CSL, 2000)

Type Introduction for Equational Rewriting. - Aart Middeldorp; Hitoshi Ohsaki (Acta Informatica, 2000)

Beyond Regularity: Equational Tree Automata for Associative and Commutative Theories. - Hitoshi Ohsaki (CSL, 2001)

Decidability and Closure Properties of Equational Tree Languages. - Hitoshi Ohsaki; Toshinori Takai (RTA, 2002)

Recognizing Boolean Closed A-Tree Languages with Membership Conditional Rewriting Mechanism. - Hitoshi Ohsaki; Hiroyuki Seki; Toshinori Takai (RTA, 2003)

ACTAS : A System Design for Associative and Commutative Tree Automata Theory. - Hitoshi Ohsaki; Toshinori Takai (RULE@RDP, 2004)

Monotone AC-Tree Automata. - Hitoshi Ohsaki; Jean-Marc Talbot; Sophie Tison; Yves Roos (LPAR, 2005)

A Sufficient Completeness Checker for Linear Order-Sorted Specifications Modulo Axioms. - Joe Hendrix; José Meseguer 001; Hitoshi Ohsaki (IJCAR, 2006)

Propositional Tree Automata. - Joe Hendrix; Hitoshi Ohsaki; Mahesh Viswanathan 001 (RTA, 2006)

Languages Modulo Normalization. - Hitoshi Ohsaki; Hiroyuki Seki (FroCoS, 2007)

Combining Equational Tree Automata over AC and ACI Theories. - Joe Hendrix; Hitoshi Ohsaki (RTA, 2008)

Tree Automata for Non-linear Arithmetic. - Naoki Kobayashi 001; Hitoshi Ohsaki (RTA, 2008)

Checking On-the-Fly Universality and Inclusion Problems of Visibly Pushdown Automata. - Nguyen Van Tang; Hitoshi Ohsaki (IEICE Trans. Fundam. Electron. Commun. Comput. Sci., 2011)

On Accelerating SMT-based Bounded Model Checking of HSTM Designs. - Weiqiang Kong; Leyuan Liu 002; Yoriyuki Yamagata; Kenji Taguchi 001; Hitoshi Ohsaki; Akira Fukuda (APSEC, 2012)

Formal Model-Based Test for AUTOSAR Multicore RTOS. - Ling Fang; Takashi Kitamura 001; Thi Bich Ngoc Do; Hitoshi Ohsaki (ICST, 2012)

Test-Case Design by Feature Trees. - Takashi Kitamura 001; Thi Bich Ngoc Do; Hitoshi Ohsaki; Ling Fang; Shunsuke Yatabe (ISoLA (1), 2012)

On Model Checking for Visibly Pushdown Automata. - Nguyen Van Tang; Hitoshi Ohsaki (LATA, 2012)

Modeling and Validating the Train Fare Calculation and Adjustment System Using VDM++. - Nguyen Van Tang; Daisuke Souma; Goro Hatayama; Hitoshi Ohsaki (VSTTE, 2012)

Formal semantics of extended hierarchical state transition matrix by CSP. - Yoriyuki Yamagata; Weiqiang Kong; Akira Fukuda; Nguyen Van Tang; Hitoshi Ohsaki; Kenji Taguchi 001 (ACM SIGSOFT Softw. Eng. Notes, 2012)

Constructing test cases for n-wise testing from tree-based test models. - Thi Bich Ngoc Do; Takashi Kitamura 001; Nguyen Van Tang; Goro Hatayama; Shinya Sakuragi; Hitoshi Ohsaki (SoICT, 2013)

A formal semantics of extended hierarchical state transition matrices using CSP#. - Yoriyuki Yamagata; Weiqiang Kong; Akira Fukuda; Nguyen Van Tang; Hitoshi Ohsaki; Kenji Taguchi 001 (Formal Aspects Comput., 2014)

Formal Specification Based Automatic Test Generation for Embedded Network Systems. - Eun-Hye Choi; Hideaki Nishihara; Takahiro Ando; Nguyen Van Tang; Masahiro Aoki; Keiichi Yoshisaka; Osamu Mizuno; Hitoshi Ohsaki (J. Appl. Math., 2014)