home > publications
SEKIZAWA Toshifusa / 関澤俊弦
-
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
(to appear)
-
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
(to appear)
-
関澤俊弦，高井利憲，田辺良則，高橋孝一：
"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.
テクニカルレポート：
AIST/CVS PS-2007-003, Feb. 2007.
"時相論理の充足可能性判定器のための論理式生成法"
-
高橋孝一，田辺良則，関澤俊弦：
"一次元セルオートマトンの有限近似解析"
コンピュータソフトウェア, Vol.23, No.3, pp.147-a57, Jul. 2006.
テクニカルレポート：
AIST/CVS PS-2005-014, August 2005. (Preliminary version)
-
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).
テクニカルレポート：
AIST/CVS PS-2005-007, Mar. 2005.
-
高橋孝一，関澤俊弦，湯浅能史，田辺良則：
「様相論理を使った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マーキングアルゴリズムの検証」
-
田辺良則，湯浅能史，関澤俊弦，高橋孝一：
「様相μ計算を利用したポインタを扱うプログラムの検証に向けて」
-
高橋孝一，湯浅能史，武山誠，関澤俊弦，田辺良則：
「自動証明系と定理証明支援系の連携によるポインタ操作プログラムの検証について」
-
高橋孝一，田辺良則，関澤俊弦，湯浅能史：
「抽象化ツールMLATについて」
-
湯浅能史，武山誠，関澤俊弦，田辺良則，高橋孝一：
「自動証明系と対話型証明支援系の連携によるポインタ操作プログラムの検証について」
-
田辺良則，湯浅能史，関澤俊弦，高橋孝一：
「様相論理を使用したヒープ検証方式」
-
田辺良則，関澤俊弦，湯浅能史，高橋孝一：
「抽象化ツールTLATの構築に向けて」
-
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)
(2005年9月21日)
-
湯浅能史，田辺良則，関澤俊弦，高橋孝一：
「時相論理による自動抽象化のための充足可能性判定手続き」
-
高橋孝一，田辺良則，関澤俊弦：
「一次元セルオートマトンの有限近似解析」
-
高橋孝一，田辺良則，高井利憲，関澤俊弦：
「ポインタ処理システムのための自動抽象化手法」
JST，CREST 「情報社会を支える新しい高性能情報処理技術」第1回公開シンポジウム (ポスター) (2004年12月14日)
-
平野聡，関澤俊弦：
「分散オブジェクト技術HORB」
COMDEX Las Vegas 2003 (2003年11月19日〜2003年11月22日)
-
細谷邦雄，関澤俊弦，岡本徹，川路紳治，湯谷明栄(A)，白木靖寛(A)，(学習院大理，東北先端研(A))：
「高移動度シリコン2次元電子系での金属・絶縁体転移と磁気抵抗」
-
関澤俊弦，岡本徹，川路紳治：
「Si-MOS 2次元電子系における強局在領域での磁気抵抗」
-
岡本徹，大河原吉貴，関澤俊弦，川路紳治：
「Si-MOSFETの巨大磁気抵抗の角度依存性」
-
Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
"Pre- and Post-conditions Expressed in Variants of the Modal μ-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, Feb. 2007.