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)
-
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.
"A Method to Generate Formulae for Tempral Logic Satisfiability Checkers"
-
Koichi Takahashi, Yoshinori Tanabe, and Toshifusa Sekizawa:
"Finite Approximation Analysis of One Dimensional Cellular Automata"
JSSST Computer Software, Vol.23, No.3, pp. 147-a57, July 2006.
(in Japanese with English abstract)
Technical Report:
AIST/CVS PS-2005-014, August 2005. (in Japanese)
-
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.
-
Koichi Takahashi, Toshifusa Sekizawa, Yoshifumi Yuasa, and Yoshinori Tanabe:
「様相論理を使ったDeutsch-Schorr-Waiteマーキングアルゴリズムの検証」
The 5th Symposium on System Verification (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.
-
Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi:
「Agda-MLAT連携による Schorr-Waiteマーキングアルゴリズムの検証」
-
Yoshinori Tanabe, Yoshifumi Yuasa, Toshifusa Sekizawa, and Koichi Takahashi:
「様相μ計算を利用したポインタを扱うプログラムの検証に向けて」
-
Koichi Takahashi, Yoshifumi Yuasa, Makoto Takeyama, Toshifusa Sekizawa, and Yoshinori Tanabe:
「自動証明系と定理証明支援系の連携によるポインタ操作プログラムの検証について」
-
Koichi Takahashi, Yoshinori Tanabe, Toshifusa Sekizawa, and Yoshifumi Yuasa:
「抽象化ツールMLATについて」
-
Yoshifumi Yuasa, Makoto Takeyama, Toshifusa Sekizawa, Yoshinori Tanabe, and Koichi Takahashi:
「自動証明系と対話型証明支援系の連携によるポインタ操作プログラムの検証について」
-
Yoshinori Tanabe, Yoshifumi Yuasa, Toshifusa Sekizawa, and Koichi Takahashi:
「様相論理を使用したヒープ検証方式」,
3rd Dependable Software Workshop (DSW'06)
, January 2006.
-
Yoshinori Tanabe, Toshifusa Sekizawa, Yoshifumi Yuasa, and Koichi Takahashi:
「抽象化ツール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),
Semtember 21, 2005.
-
Yoshifumi Yuasa, Yoshinori Tanabe, Toshifusa Sekizawa, and Koichi Takahashi:
「時相論理による自動抽象化のための充足可能性判定手続き」
-
Koichi Takahashi, Yoshinori Tanabe, and Toshifusa Sekizawa:
"Finite Approximation Analysis of One Dimensional Cellular Automata"
-
Koichi Takahashi, Yoshinori Tanabe, Toshinori Takai, and Toshifusa Sekizawa:
「ポインタ処理システムのための自動抽象化手法」,
JST,CREST program
"New High-Performance Information Processing Technology Supporting Information-Oriented Society"
1st symposium, December 2004.
-
Satoshi Hirano, and Toshifusa Sekizawa:
"Distributed Object-Oriented Technology HORB"
COMDEX Las Vegas 2003, November 19, 2003 - November 22, 2003.
-
K. Hosoya, T. Sekizawa, T. Okamoto, S. Kawaji, A. Yutani, and Y. Shiraki:
"Metal-Insulator Transition and Magnetoresistance in High Mobility Silicon Two-Dimensional Electron System"
-
T. Sekizawa, T. Okamoto, and S. Kawaji:
"Magnetoresistance in Strongly Localized States in Si-MOSFETs"
-
T. Okamoto, Y. Ohkawara, T. Sekizawa, and S. Kawaji:
"Giant Magnetoresistance in Si-MOSFETs in Tilted Magnetic Fields"
-
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.