高橋 孝一

一次元セルオートマトンの有限近似解析 

コンピュータソフトウェア 23(3) 147-157 2006年  

時相論理の充足可能性判定器のための論理式生成法 

電子情報通信学会論文誌 D-I J89-D(4) 642-650 2006年  

モデル検査技術適用事例研究会の報告 

第5回クリティカルソフトウェアワークショップ（WOCS） 189-191 2005年  

一次元セルオートマトンの有限近似解析(Preliminary Version) 

算譜科学研究速報 2005年  

時相論理の充足可能性判定器のための性能評価法 

算譜科学研究速報 2005年  

A Decision Procedure for Alternation-free Two-way Modal mu-calculus 

算譜科学研究速報 2005年  

Precondisions of properties described in CTL for statementsmanipulating pointers 

算譜科学研究速報 2005年  

BDDを用いた2方向CTL論理式充足可能性決定手続きの実装 

コンピュータソフトウェア 22(3) 154-166 2005年  

抽象化を用いた検証ツールの調査 

産業技術総合研究所算譜科学グループ研究速報 2003年  

暗号通信手順の安全性自動検証技術に関する研究成果報告書 

AIST PROGTAMMING SCIENCE GROUP TECHNICAL REPORT 2003年  

モデル検査器を用いた自動検針システムの仕様検証 

産業技術総合研究所算譜科学グループ研究速報 2003年  

Verification of Authentication Protocols Based on the Binding Relation 

(SOFTWARE SECURITY - THEORIES AND SYSTEMS, LNCS2609) 2003年  

束縛関係に基づく認証プロトコルの検証 

コンピュータソフトウェア 20(3) 17-29 2003年  

Searching for Mutual Exclusion Algorithms using BDDs 

(PROGRESS IN DISCOVERY SCIENCE, LNAS2281) 2002年  

モデル検査系を用いたプログラム発見 

人工知能学会誌 16(5) 648-654 2001年  

標数2のある体上の代数方程式の求解 

コンピュータソフトウエア 18(3) 29-33 2001年