Koichi Takahashi

My email address is k.takahashi at aist.go.jp ( gnupg public key )

My research interest is on proving by machine. My current topic is abstract model checking.

Links

• Research Center for Verification and Semantics | AIST
• My research group member: Toshifusa Sekizawa
• (Internal: Schedule | Group intra | AIST intra )

Awards

• 日本ソフトウェア科学会第1回解説論文賞. (田辺良則，高井利憲，高橋孝一: 抽象化を用いた検証ツール. コンピュータソフトウェア，Vol.22, No.1 (2005), pp.2-44.)
• ICSEA 2007 Best Paper Award. (Osamu Takaki, Takahiro Seino, Izumi Takeuti, Noriaki Izumi, Koichi Takahashi. Verification Algorithm of Evidence Life Cycles in Extended UML Activity Diagrams. International Conference on Software Engineering Advances (ICSEA), 2007.)

Publications

Refereed

• 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.-,May. 2009.
• 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.-,May. 2009.
• Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, Koichi Takahashi: Verification of the Deutsch-Schorr-Waite Marking Algorithm with Modal Logic. Second International Conference, Verified Software: Theories, Tools, Experiments (VSTTE 2008), LNCS 5295, pp.115--129, 2008
• Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya: A decision procedure for alternation-free modal $\mu$-calculi. In C. Areces, R. Goldblatt, editors, Advances in Modal Logic, Volume 7, College Publications, pages 341-362, London, 2008.
• Toshifusa Sekizawa, Yoshinori Tanabe, Yoshifumi Yuasa, and Koichi Takahashi. MLAT: A Tool for Heap Analysis based on Predicate Abstraction by Modal Logic. The IASTED International Conference on Software Engineering (SE 2008), (to appear).
• Osamu Takaki, Takahiro Seino, Izumi Takeuti, Noriaki Izumi, Koichi Takahashi: Quality Improvement of Workflow Diagrams Based on Passback Flow Consistency. ICEIS (3-2) 2008: 351-35
• Osamu Takaki, Izumi Takeuti, Takahiro Seino, Noriaki Izumi, Koichi Takahashi: Incremental Verification of Large ScaleWorkflows Based on Extended Correctness. ICSEA 2008: 478-487
• Osamu Takaki, Takahiro Seino, Izumi Takeuti, Noriaki Izumi, Koichi Takahashi: Workflow Diagrams Based on Evidence Life Cycles. JCKBSE 2008: 145-154
• 高木 理,清野 貴博 ,竹内 泉 ,和泉 憲明 ,高橋 孝一. UMLアクティビティ図に対する事象部分グラフ抽出および事象独立性検証アルゴリズム. ソフトウェアエンジニアリング最前線2007，近代科学社. pp. 153-164．2007
• Osamu Takaki, Takahiro Seino, Izumi Takeuti, Noriaki Izumi, Koichi Takahashi. Verification Algorithm of Evidence Life Cycles in Extended UML Activity Diagrams. International Conference on Software Engineering Advances (ICSEA), 2007.
• 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.
• Toshifusa Sekizawa, Toshinori Takai, Yoshinori Tanabe, Koichi Takahashi: A Method to Generate Formulae for Temporal Logic Satisfiability Checkers. Electronics and Communications in Japan, Part II, Vol. 90, Issue 11, pp. 98-108, October 2007. (English version of the next paper).
• 関澤俊弦, 高井利憲, 田辺良則, 高橋孝一: 時相論理の充足可能性判定器のための論理式生成法. 電子情報通信学会論文誌(D), Vol.J89-D, No.4, pp.642-650, Apr. 2006. (Preliminary Version is AIST/CVS PS-2005-015 .)
• 高橋孝一, 田辺良則, 関澤俊弦: 一次元セルオートマトンの有限近似解析. コンピュータソフトウェア, Vol.23, No.3, pp.147-157, Jul. 2006. (Preliminary Version is here .)
• 田辺良則, 高橋孝一, 山本光晴, 佐藤貴洋, 萩谷昌己: BDDを用いた2方向CTL論理式充足可能性決定手続きの実装. コンピュータソフトウェア, Vol.22, No.3, 2005, pp.154-166.
• Yoshinori Tanabe, Koichi Takahashi, Mitsuharu Yamamoto, Akihiko Tozawa, and Masami Hagiya: A Decision Procedure for the Alternation-free Two-way Modal mu-calculus. TABLEAUX 2005, Lecture Notes in Artificial Intelligence, Vol.3702, 2005, pp.277-291.
• 田辺良則，高井利憲，高橋孝一: 抽象化を用いた検証ツール. コンピュータソフトウェア，Vol.22, No.1 (2005), pp.2-44.
• 萩谷昌己, 竹村亮, 高橋孝一, 齋藤孝道: 束縛関係に基づく認証プロトコルの検証, コンピュータソフトウェア, Vol.20, No.3, 2003, pp.17-29.
• Masami Haigya, Ryo Takemura, Koichi Takahashi, and Takamichi Saito: Verification of Authentication Protocols Based on the Binding Relation. Software Security -- Theories and Systems, Mext-NSF-JSPS Internationa Symposium, ISSS 2002, Tokyo, Japan, November 2002, Revised papers, Lecture Notes in Computer Science, Springer, Vol.2609, 2003, pp.299-316.
• Koichi Takahashi and Masami Hagiya: Searching for Mutual Exclusion Algorithms Using BDDs. Progress in Discovery Science, (Setsuo Arikawa and Ayumi Shinohara Eds.), Lecture Notes in Artificial Intelligence, Vol.2281, 2002, pp.1-18.
• 萩谷昌己, 高橋孝一: モデル検査系を用いたプログラム発見, 人工知能学会誌, Vol.16, No.5, 2001, pp.648-654.
• 高橋孝一, 萩谷昌己: 正則表現を用いた並列ごみ集めの抽象モデル検査, 情報処理学会論文誌プログラミング, Vol.42, No.SIG2(PRO9), 2001, pp.61-70.
• 山本光晴, 高橋孝一, 萩谷昌己, 西崎真也, 玉井哲雄: グラフ探索アルゴリズムの発展とその応用, コンピュータソフトウェア別冊, ソフトウェア発展, Vol.19, No.0, 2001, pp.92-108.
• 萩谷昌己, 戸沢晶彦, 高橋孝一, 西崎真也: Javaのクラスローダ制約の定式化, 情報処理学会論文誌プログラミング, Vol.41, No.SIG4(PRO7), 2000, pp.79-87.
• Koichi Takahashi and Masami Hagiya: Proving as Editing HOL Tactics. Informal proceedings of the Workshop on User Interfaces for Theorem Provers, UITP'98 (Roland Backhouse, ed.), Eindhoven University of Technology, 1998, pp.157-164. Also in Formal Aspects of Computing, Vol.11, No.3, 1999, pp.343-357.
• 萩谷昌己, 高橋孝一: 「計算＝編集」パラダイムに従うHOLタクティクのためのEmacsインタフェース. インタラクティブシステムとソフトウェアV, レクチャーノート/ソフトウェア学, 近代科学社, Vol.18, 1997, pp.123-128.
• Mitsuharu Yamamoto, Koichi Takahashi, Masami Hagiya, Shin-ya Nishizaki, and Tetsuo Tamai: Formalization of Graph Search Algorithms and Its Applications. Theorem Proving in Higher Order Logics, 11th International Conference, TPHOLs'98, Canberra, Australia, September/October 1998, Proceedings (Jim Grundy, Malcolm Newey, eds.) Lecture Notes in Computer Science, Springer-Verlag, Vol.1479, 1998, pp.479-496.

Invited

• 高橋 孝一 , 高井 利憲 . システム検証における数理的手法−組込みシステムへの適用事例. システム・制御・情報, 51 巻 9 号 393 頁〜 398 頁, 2007.
• 高橋 孝一. モデル検査で状態爆発をいかに抑えるか. 組み込みソフトウェア２００７ モデルに基づく開発方法論のすべて. 日経BP社. 140 頁〜 147 頁. 2006.
• Masami Hagiya, Koichi Takahashi, Mitsuharu Yamamoto, and Takahiro Sato: Analysis of Synchronous and Asynchronous Cellular Automata using Abstraction by Temporal Logic. FLOPS2004: The Seventh Functional and Logic Programming Symposium, Lecture Notes in Computer Science, Vol.2998, 2004, pp.7-21.
• Masami Hagiya and Koichi Takahashi: Discovery and Deduction. Discovery Science, Third International Conference, DS 2000, (Setsuo Arikawa and Shinichi Morishita Eds.), Lecture Notes in Artificial Intelligence, Vol.1967, 2000, pp.17-37.

Thesis

• Koichi Takahashi: Abstraction and Search in Verification by State Exploration. Ph.D thesis, The University of Tokyo, January 2002. ( pdf )

Unrefereed

• Yoshinori Tanabe, Toshinori Takai, Toshifusa Sekizawa, 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.
• Mitsuharu Yamamoto, Yoshinori Tanabe, Koichi Takahashi, and Masami Hagiya: Abstraction of Graph Transformation Systems by Temporal Logic and Its Verification. IFIP TC2, Verified Software: Theories, Tools, Experiments, 2005.
• Koichi Takahashi and Masami Hagiya: Abstraction of Graph Transformation Using Temporal Formulas. Workshop on Model-Checking for Dependable Software-Intensive Systems, International Conference on Dependable Systems and Networks, DSN2003, pp.W-65-66, 2003.
• Koichi Takahashi and Masami Hagiya: Formal Proof of Abstract Model Checking of Concurrent Garbage Collection. Workshop on Thirty Five years of Automath, Informal Proceedings (Fairouz Kamareddine Ed.), Heriot-Watt University, Edinburgh, April, 2002, pp.115-126.
• Masami Hagiya and Koichi Takahashi: Searching for Synchronization Algorithms using BDDs. IPSJ PRO, Information Processing Society of Japan, January 2001.
• Koichi Takahashi and Masami Hagiya: Abstraction of Link Structures by Regular Expressions and Abstract Model Checking of Concurrent Garbage Collection. First Asian Workshop on Programming Languages and Systems, National University of Singapore, 2000, pp.1-8.
• Koichi Takahashi, Yozo Toda, and Masami Hagiya: Nonce Analysis and Strand Space Model. JSSST 2000, Japan Society for Software Science and Technology, 2000.

under construction. sorry.