Toshifusa Sekizawa

著書 (分担執筆を含む)

• 関澤俊弦, 高橋孝一:
  "モデル検査によるシステム検証,"
  日本信頼性学会 (REAJ) 「新版 信頼性ハンドブック」, Chapter V, Section D-4, July 2014.
• 岡野浩三, 関澤俊弦 編:
  "ソフトウェア工学の基礎 XX FOSE2013,"
  近代科学社, December 2013.
• 関澤俊弦，高橋孝一:
  "モデル検査（総論）,"
  電子情報通信学会 ハンドブック「知識ベース」 7群1編2章4, pp.28-34, 2010.
• 高橋孝一，関澤俊弦:
  "抽象化"
  電子情報通信学会 ハンドブック「知識ベース」 7群1編3章1, pp.3-9, 2010.

論文誌

• Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, and Shinji Kusumoto:
  "Parallel Multiple Counter-Examples Guided Abstraction Loop - Applying to Timed Automaton -,"
  International Journal of Informatics Society (IJIS), Vol. 8, No. 2, pp.103-116, September 2016.
• Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto:
  "Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects,"
  International Journal of Informatics Society (IJIS), Vol. 6, No.2, pp. 79-87, November 2014.
• Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto:
  "Verification of Safety Properties of a Program for Line Tracing Robot using a Timed Automaton Model,"
  Special Issue of the International Journal of Informatics Society (IJIS), Vol. 5, No. 3, pp.147-155, March 2014.
• [解説論文]
  土屋達弘，関澤俊弦:
  "制御システム分野におけるモデル検査の応用,"
  システム制御情報学会 「システム/制御/情報」, 第57巻, 第5号, pp.195-200, 2013.
• Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi, and Kazuko Takahashi:
  "Probabilistic Symmetry Reduction for a System with Ring Buffer"
  The IEICE Transactions on Information and Systems, Special Section on Formal Approach,
  Vol. E94-D, No. 5, pp. 967-975, May 2011.
• Toshifusa Sekizawa, Takashi Toyoshima, Koichi Takahashi, and Kazuko Takahashi:
  "Probabilistic Symmetry Reduction for a System with Ring Buffer"
  The IEICE Transactions on Information and Systems, Special Section on Formal Approach,
  Vol. E94-D, No. 5, pp. 967-975, May 2011.
• Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Koichi Takahashi, and Tohru Kikuno:
  "Probabilistic Model Checking of the One-Dimensional Ising Model"
  The IEICE Transactions on Information and Systems, Special Section on Formal Approach, Vol. E92-D, No. 5, pp. 1003-1011, May 2009.
• Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
  "Pre- and Post-conditions Expressed in Variants of the Modal mu-calculus"
  The IEICE Transactions on Information and Systems, Special Section on Formal Approach, Vol. E92-D, No. 5, pp. 995-1002, May 2009.
• Toshifusa Sekizawa, Toshinori Takai, Yoshinori Tanabe, and Koichi Takahashi:
  "A Method to Generate Formulas for Temporal Logic Satisfiability Checkers"
  Electronics and Communications in Japan, Part II, Vol. 90, Issue 11, pp. 98-108, October 2007.
  (Technical Report: AIST/CVS PS-2007-004, Feb. 2007)
• 関澤俊弦，高井利典，田辺良則，高橋孝一:
  "時相論理の充足可能性判定のための論理式生成法"
  電子情報通信学会論文誌(D), Vol.J89-D, No.4, pp. 642-650, April 2006.
  (Technical Report: AIST/CVS PS-2005-015, September 2005. (Preliminary version))
• 高橋孝一，田辺良則，関澤俊弦:
  "一次元セルオートマトンの有限近似解析"
  コンピュータソフトウェア, Vol.23, No.3, pp. 147-157, July 2006.
  (Technical Report: AIST/CVS PS-2005-014, August 2005.)

国際会議

• Ryo Watanabe, Kozo Okano, and Toshifusa Sekizawa:
  "Towards Verification of Robot Design for Self-localization,"
  Thirteenth Haifa Verification Conference (HVC 2017), LNCS, Vol. 10629, pp. 245-248, 2017. (Haifa, Israel)
• Kozo Okano, Satoshi Harauchi, Toshifusa Sekizawa, Shinpei Ogata, and Shin Nakajima:
  "Equivalence Checking of Java Methods - Towards Ensuring IoT Dependability -,"
  The 7th International Workshop on Internet on Things: Privacy, Security and Trust (IoTPST 2017). (Vancouver, Canada)
• Toshifusa Sekizawa, Makoto Fujiwara, and Koichiro Watanabe:
  "A Case Study: Verification of an Embedded System using Abstraction Refinement with Requirements,"
  In Proceedings of COMPSAC 2016: The 2nd IEEE International Workshop on Dependable Software and Applications (DSA 2016), pp. 490-493, June 2016. (Atlanta, the United States)
• Kozo Okano, Takeshi Nagaoka, Toshiaki Tanaka, Toshifusa Sekizawa, and Shinji Kusumoto:
  "Parallel Multiple Counter-Examples Guided Abstraction Loop to Timed Automaton,"
  International Workshop on Informatics 2015 (IWIN2015), pp. 153-160, September 2015. (Amsterdam, Netherlands)
• Toshifusa Sekizawa, Fumiya Otsuki, Kazuki Ito, and Kozo Okano:
  "Behavior Verification of Autonomous Robot Vehicle in Consideration of Errors and Disturbances,"
  In Proceedings of COMPSAC 2015 Workshop: The 1st IEEE International Workshop on Dependable Software and Applications (DSA 2015), pp. 550-555, July 2015. (Taichung, Taiwan)
• Kozo Okano, and Toshifusa Sekizawa:
  "Safety Verification of Multiple Autonomous Systems by Formal Approach,"
  In Proceedings of International Conference on Computer Safety, Reliability, and Security (SAFECOMP) 2014 Workshops: ASCoMS, DECSoS, DEVVARTS, ISSE, ReSA4CI, SASSUR, September 2014. (Florence, Italy)
  Lecture Note in Computer Science (LNCS), Vol. 8696, pp. 11-18, 2014.
• Toshifusa Sekizawa, and Tsugu Kotorii:
  "A Case Study: Verification of Specifications of an Embedded System and Generation of Verification Items using Pairwise Testing",
  In Proceedings of the 20th Asia-Pacific Software Engineering Conference (APSEC 2013), pp. 146-151, December 2013. (Bangkok, Thailand)
• Toshifusa Sekizawa, Kozo Okano, Ayako Ogawa, and Shinji Kusumoto:
  "Verification of a Control Program for a Line Tracing Robot using UPPAAL Considering General Aspects",
  International Workshop on Informatics 2013 (IWIN2013), pp. 155-162, September 2013. (Stockholm, Sweden)
• Kozo Okano, Toshifusa Sekizawa, Hiroaki Shimba, Hideki Kawai, Kentaro Hanada, Yukihiro Sasaki, and Shinji Kusumoto:
  "Verification of Safety Property of Line Tracer Program using Timed Automaton Model",
  International Workshop on Informatics 2012 (IWIN2012), pp. 136-142, September 2012. (Chamonix Mont-Blanc, France)
• Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi:
  "Verification of the Deutsh-Schorr-Waite marking algorithm with Modal Logic"
  Second IFIP Working Conference on Verified Software: Theories, Tools, and Experiments ( VSTTE'08 ), Lecture Notes in Computer Science, Vol. 5295, pp. 115-129, Springer, October 2008. (Tronto, Canada)
• Toshifusa Sekizawa, Yoshinori Tanabe, Yoshifumi Yuasa, and Koichi Takahashi:
  "MLAT: A Tool for Heap Analysis Based on Predicate Abstraction by Modal Logic"
  Proceedings of the IASTED International Conference on Software Engineering (SE 2008), pp. 310-317, February 2008. (Innsbruck, Austria)
• Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi:
  "Analyzing the One Dimensional Ising Model by Probabilistic Model Checking"
  Proceedings of the IASTED Asian Conference on Modelling and Simulation (AsiaMS 2007), pp. 199-204, October 2007. (Beijing, China)
• Yoshinori Tanabe, Toshinori Takai, Toshifusa Sekizawa and Koichi Takahashi:
  "Preconditions of Properties Described in CTL for Statements Manipulating Pointers"
  Supplemental Volume of the 2005 International Conference on Dependable Systems and Networks (DSN-2005), June 28 - July 1, 2005, pp. 228-234. (Yokohama, Japan).
  Technical Report： AIST/CVS PS-2005-007, March 2005.

博士論文

• Toshifusa Sekizawa
  "A Study of Model Checking with Emphasis on Program Verification and Probabilistic Analysis"
  大阪大学 大学院情報科学研究科, 2009年1月.

研究会

• 矢吹光，関澤俊弦:
  "自己位置推定をするロボットの確率的な振舞いの協調解析に向けて,"
  JSSST FOSE2017, Nov. 2017
• 渡邊亮，岡野浩三，関澤俊弦:
  "モデル検査を用いたロボット設計の検証,"
  JSSST FOSE2017, Nov. 2017
• 渡邊亮，岡野浩三 ，関澤俊弦:
  "自己位置推定を行なうロボット設計の検証に向けて,"
  IPSJ/SIGSE SES2017 ワークショップ「ソフトウェアと不確かさ」, August, 2017.
• 岡野浩三，原内聡，小形真平，関澤俊弦，小原岳士:
  "Javaのメソッド等価性判定とその応用,"
  電子情報通信学会技術研究報告 IEICE-SS2016-65, Vol. 116, No. 512, pp.31-36, March 2017.
• 渡辺誠人，岡野浩三，関澤俊弦:
  "ペアワイズ法に基づいた検証項目の生成とモデル検査による組み込みシステムの検証に向けて,"
  IPSJ/SIGSE ウィンターワークショップ・イン・飛騨高山, January, 2017.
• 田幸玄陽，小形真平，岡野浩三，関澤俊弦:
  "Kuromojiと構文解析による要求仕様書から状態遷移系への自動変換の試み,"
  IPSJ/SIGSE ウィンターワークショップ・イン・飛騨高山, pp. 45-46, January, 2017.
• 渡邊亮，岡野浩三，関澤俊弦:
  "二次元系における自己位置推定の振舞い検証に向けて,"
  JSSST FOSE2016, ソフトウェア工学の基礎XXIII, pp. 275-276, Dec. 2016.
• 小林佳正，岡野浩三，関澤俊弦:
  "移動時間を考慮に入れた自律移動ロボットの確率的な振舞い検証に向けて,"
  JSSST 第23回 ソフトウェア工学の基礎ワークショップ (FOSE2016), Dec. 2016. (ポスター)
• 小林佳正，岡野浩三，関澤俊弦
  "確率時間オートマトンを用いた自律移動ロボットの振舞いのモデル化,"
  情報処理学会研究報告 Vol. 2016-SE-192, No. 14, June 2016.
• 関澤俊弦，岡野浩三:
  "一次元系における自己位置推定の振舞い検証に向けて,"
  電子情報通信学会技術研究報告 SS2015-100, Vol. 115, No. 508, pp.145-150, March 2016.
• 遠藤健，小形真平，岡野浩三，関澤俊弦:
  "自然語要求仕様記述の形式検証に向けて - 話題沸騰ポットのモデル検査に向けて -,"
  IPSJ/SIGSE ウィンターワークショップ 2016・イン・逗子, pp. 3-4, February 2016.
• 小林佳正，岡野浩三，関澤俊弦:
  "時間的性質を考慮に入れた自律移動ロボットの誤差検出と振舞い検証に向けて,"
  JSSST 第22回 ソフトウェア工学の基礎ワークショップ (FOSE2015), November, 2015. (poster)
• 大槻文也，伊藤和己，岡野浩三，関澤俊弦:
  "自律移動ロボットの誤差検出と振舞い検証に向けて,"
  IPSJ/SIGSE ウィンターワークショップ 2015・イン・宜野湾, pp. 69-70, January 2015.
• 関澤俊弦，小鳥井継:
  "組込みシステムの仕様検証とペアワイズ法を用いた検証項目の生成,"
  JSSST 第20回 ソフトウェア工学の基礎ワークショップ (FOSE2013), November, 2013. (poster)
• 岡野浩三, 関澤俊弦, 榛葉浩章, 楠本真二:
  "UPPAALによるライントレーサの安全性検証のケーススタディ,"
  ソフトウェアエンジニアリングシンポジウム2012 (SES2012), August 2012.
• 関澤俊弦，高橋孝一，高橋和子：
  "リングバッファ上の系に対する確率的対称性簡約,"
  ウィンターワークショップ 2012・イン・琵琶湖, IPSJ Symposium Series Vol.2012, No.1, pp.115-116, January 2012.
• 河井秀樹，岡野浩三，関澤俊弦：
  "ライントレーサの定量的評価および検証に向けて,"
  ウィンターワークショップ 2012・イン・琵琶湖, IPSJ Symposium Series Vol.2012, No.1, pp.113-114, January 2012.
• 関澤俊弦，高橋孝一，高橋和子:
  "ケーススタディ： Hermanの確率的自己安定化アルゴリズムの状態削減と検証,"
  ディペンダブルシステムワークショップ & シンポジウム (DSW & DSS 2011), December 2011.
• 豊島祟士，高橋和子，関澤俊弦:
  "Symmetry Reductionを使ったAISの確率付きモデル検査,"
  電子情報通信学会技術研究報告 SS2009-63, Vol. 109, No. 456, pp.91-96, March 2010.
• 関澤俊弦，小池憲史，小池隆，篠崎孝一，西原秀明，早水公二:
  "シナリオに基づくモデル検査導入手法の策定 - はじめての現場マニュアル -,"
  第６回 ディペンダブルシステムシンポジウム (DSS2009), December 2009.
• 高橋孝一，関澤俊弦，湯浅能史，田辺良則:
  "様相論理を使ったDeutsch-Schorr-Waiteマーキングアルゴリズムの検証,"
  第五回 システム検証の科学技術シンポジウム (SSV 2008), November 2008.
• Toshifusa Sekizawa, Tatsuhiro Tsuchiya, Tohru Kikuno, and Koichi Takahashi:
  "A Case Study: Analyzing the One Dimensional Ising Model by Probabilistic Model Checking,"
  5th VERITE (JAIST/TRUST-AIST/CVS joint workshop on VERIfication TEchnology), March 2008.
• 湯浅能史，田辺良則，関澤俊弦，高橋孝一:
  "Agda-MLAT連携による Schorr-Waiteマーキングアルゴリズムの検証,"
  日本ソフトウェア科学会 第２４回大会, September 2007.
• 田辺良則，湯浅能史，関澤俊弦，高橋孝一:
  "様相μ計算を利用したポインタを扱うプログラムの検証に向けて,"
  第９回 プログラミング言語ワークショップ (PPL 2007), March 2007.
• 高橋孝一，湯浅能史，武山誠，関澤俊弦，田辺良則:
  "自動証明系と定理証明支援系の連携によるポインタ操作プログラムの検証について,"
  Theorem Proving and Provers (TPP) Meeting, November 2006.
• 高橋孝一，田辺良則，関澤俊弦，湯浅能史:
  "抽象化ツールMLATについて,"
  第三回システム検証の科学技術シンポジウム, October 2006.
• 湯浅能史，武山誠，関澤俊弦，田辺良則，高橋孝一:
  "自動証明系と対話型証明支援系の連携によるポインタ操作プログラムの検証について,"
  日本ソフトウェア科学会 第２３回大会, September 2006.
• 田辺良則，湯浅能史，関澤俊弦，高橋孝一:
  "様相論理を使用したヒープ検証方式,"
  第３回 ディペンダブルソフトウェアワークショップ (DSW'06), January 2006.
• 田辺良則，関澤俊弦，湯浅能史，高橋孝一:
  "抽象化ツールTLATの構築に向けて,"
  第2回システム検証の科学技術シンポジウム, October 21, 2005 (ポスター)
  (Technical Report： AIST/CVS PS-2005-017, pp. 101-101, October 2005. (in Japanese))
• Koichi Takahashi, Yoshinori Tanabe, Toshifusa Sekizawa and Yoshifumi Yuasa:
  "Abstraction of programs in PML (Pointer Manipulating Language),"
  JAIST/TRUST - AIST/CVS joint workshop on verification technology (VERITE) (oral presentation), September 21, 2005.
• 湯浅能史，田辺良則，関澤俊弦，高橋孝一:
  "時相論理による自動抽象化のための充足可能性判定手続き,"
  日本ソフトウェア科学会 第22回大会, September 13, 2005.
• 高橋孝一，田辺良則，関澤俊弦:
  "一次元セルオートマトンの有限近似解析,"
  日本ソフトウェア科学会 第２２回大会, September 13, 2005.
• 高橋孝一，田辺良則，高井利憲，関澤俊弦:
  "ポインタ処理システムのための自動抽象化手法,"
  JST，CREST 「情報社会を支える新しい高性能情報処理技術」第1回公開シンポジウム (ポスター), December 14, 2004.
• 平野聡，関澤俊弦:
  "分散オブジェクト技術HORB,"
  COMDEX Las Vegas 2003, November 19, 2003 - November 22, 2003.
• 細谷邦雄，関澤俊弦，岡本徹，川路紳治，湯谷明栄(A)，白木靖寛(A)，(学習院大理，東北先端研(A)):
  "高移動度シリコン2次元電子系での金属・絶縁体転移と磁気抵抗,"
  日本物理学会講演概要集, Vol.53, No.1-3(19980310), p.536, March 30, 1998.
• 関澤俊弦，岡本徹，川路紳治:
  "Si-MOS 2次元電子系における強局在領域での磁気抵抗,"
  日本物理学会講演概要集, Vol.52, No.1-2(19970317), p.148, March 28, 1997.
• 岡本徹，大河原吉貴，関澤俊弦，川路紳治:
  "Si-MOSFETの巨大磁気抵抗の角度依存性,"
  日本物理学会講演概要集，Vol.51,　No.2, p.184, March, 1996.

テクニカルレポート

• Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
  "Pre- and Post-conditions Expressed in Variants of the Modal mu-calculus,"
  AIST/CVS PS-2008-009, April 2008.
• Toshifusa Sekizawa, Yoshinori Tanabe, Yoshifumi Yuasa, and Koichi Takahashi:
  "MLAT: Modal Logic Abstraction Tool,"
  AIST/CVS PS-2007-004, February 2007.