General Models and Completeness of First-Order Modal µ-calculus. - Ryo Kashima; Keishi Okamoto (J. Log. Comput., 2008)

Formal Validation and Requirements Management Based on the Jackson's Reference Model for Requirements and Specifications. - Takashi Kitamura 001; Keishi Okamoto; Makoto Takeyama (PRDC, 2010)

Formal Verification in a First-Order Extension of Modal μ-calculus. - Keishi Okamoto (Inf. Media Technol., 2010)

Automated Route Planning for Milk-run Transport Logistics Using Model Checking. - Takashi Kitamura 001; Keishi Okamoto (ICNC, 2012)

Automated Route Planning for Milk-Run Transport Logistics with the NuSMV Model Checker. - Takashi Kitamura 001; Keishi Okamoto (IEICE Trans. Inf. Syst., 2013)

Warpage analysis of organic substrates for 2.1D packaging. - Sayuri Kohara; Keishi Okamoto; Hirokazu Noma; Kazushige Toriyama; Hiroyuki Mori (3DIC, 2015)

A Bayesian Approach to Argument-Based Reasoning for Attack Estimation. - Hiroyuki Kido 001; Keishi Okamoto (IJCAI, 2017)

Balancing Between Cognitive and Semantic Acceptability of Arguments. - Hiroyuki Kido 001; Keishi Okamoto (KSEM, 2017)

Deriving of Time Constants in Timed Automata for Hazard Transition Sequences for STAMP/STPA. - Kozo Okano; Pan Yang 015; Shinpei Ogata; Keishi Okamoto (KES, 2020)

Bayes Meets Entailment and Prediction: Commonsense Reasoning with Non-monotonicity, Paraconsistency and Predictive Accuracy. - Hiroyuki Kido 001; Keishi Okamoto (CoRR, 2020)

A Bounded Model Checker for Timed Automata and Its Application to LTL Properties. - Kozo Okano; Maiko Onishi; Jo Otsuka; Shinpei Ogata; Toshifusa Sekizawa; Keishi Okamoto; Daisuke Bekki (KES, 2022)