| IEICE Technical Committee Submission System Conference Schedule |
Online Proceedings [Sign in] Tech. Rep. Archives |
All Technical Committee Conferences (Searched in: All Years)
| Committee | Date Time | Place | Paper Title / Authors | Abstract | Paper # | |
| VLD | 2014-03-05 15:45 |
Okinawa | Okinawa Seinen Kaikan | A Case Study of Symbolic Model Checking for Verilog-HDL Hardware Design Tomoyuki Yokogawa, Daichi Higashiyama (Okayama Pref. Univ.), Masafumi Kondo (Kawasaki Univ. of Medical Welfare), Yoichiro Sato, Kazutami Arimoto (Okayama Pref. Univ.)  VLD2013-166 |
In this paper, we show a case study where a design of 8bit microcomputer M8R, which is described by Verilog-HDL, is veri... [more] | VLD2013-166 pp.177-182 |
| SS, MSS | 2014-01-31 09:55 |
Aichi | Bounded model checking based in SMT for CISC embedded assembly programs Atsushi Takeshita, Junpei Kobashi, Satoshi Yamane (Kanazawa Univ.) MSS2013-62 SS2013-59 |
In this paper,we describe the method of verification by bounded model checking based in SMT using Code Block for embedde... [more] | MSS2013-62 SS2013-59 pp.65-70 |
|
| IN, NV (Joint) |
2013-07-19 15:15 |
Hokkaido | Hokkaido Univ. Faculty of Eng. Academic Lounge 3 | Model Checking of OpenFlow Network with Abstraction of Packets Based on Symbolic Execution Yutaka Yakuwa, Nobuyuki Tomizawa, Toshio Tonouchi (NEC) IN2013-54 |
We propose a verification method of the OpenFlow network with the model checking, which can detect a loop routing and so... [more] | IN2013-54 pp.107-112 |
| KBSE | 2013-03-15 11:25 |
Tokyo | Shibaura Institute of Technology | A proposal on architecture based verification case Shuichiro Yamamoto (Nagoya Univ.) KBSE2012-82 |
Although formal method is attracted to verify system correctness, it is not practical to verify every property of system... [more] | KBSE2012-82 pp.79-83 |
| DC | 2012-12-14 17:00 |
Fukui | Aossa (Fukui) | Verification of Automatic Block System for Single Line Using SMT Solver Natsuki Terada (RTRI) DC2012-79 |
Formal methods are expected to increase reliability of software, including that of signaling systems. We modeled the sp... [more] | DC2012-79 pp.31-36 |
| SS, IPSJ-SE | 2012-11-01 13:15 |
Hiroshima | Hiroshima City University | Application of formal methods to network behavior dependent systems Nobuaki Yoshida (ASTEM), Han-Myung Chang, Atsushi Sawada (Nanzan Univ.), Yukihiro Nakamura (ASTEM) SS2012-39 |
In this paper, we study application of formal methods to“mobile systems”, which consist of wireless devices distributed ... [more] | SS2012-39 pp.35-40 |
| MSS | 2012-03-09 13:00 |
Tokyo | JAIST Tokyo Satellite | Formal Verification of a Telephone System with a Concierge Server Keito Kurono, Aya Maeda, Yoshinobu Kawabe (Aichi Inst. Tech.) MSS2011-84 |
To avoid becoming a victim of phone fraud, it is important to check whether a caller is a scammer or not. Yamamoto et.a... [more] |
MSS2011-84 pp.61-66 |
| ISEC, LOIS | 2011-11-14 15:35 |
Osaka | Osaka Electro-Communication University | Formalization and Verification of Arithmetic Algorithms by Mizar Yoshiki Aoki, Hiroyuki Okazaki, Yasunari Shidama (Shinshu Univ.) ISEC2011-44 LOIS2011-38 |
In this report, we formalize some number theoretical algorithms, Euclidean Algorithm and Extended Euclidean Algorithm ... [more] |
ISEC2011-44 LOIS2011-38 pp.69-74 |
| ISEC, LOIS | 2011-11-15 14:15 |
Osaka | Osaka Electro-Communication University | Symbolic Criterion of EUC Secure Message Authentication for Multi-Message Protocols Itsuki Suzuki, Maki Yoshida, Toru Fujiwara (Osaka Univ.) ISEC2011-57 LOIS2011-51 |
A protocol is said to be EUC secure if it can be securely composed with arbitrary protocols which use the same setup. ... [more] |
ISEC2011-57 LOIS2011-51 pp.155-162 |
| KBSE | 2011-11-11 13:20 |
Nagano | Shinshu Univ. | A Formal Verification Method by Transforming UML Models of Web Applications Takahiko Ohsuga (Waseda Univ.), Kouichi Ono (IBM), Yoshiaki Fukazawa (Waseda Univ.) KBSE2011-49 |
Model checking techniques are being applied to application software for formal verifications. Regarded as results of dev... [more] | KBSE2011-49 pp.79-84 |
| SS | 2011-10-28 11:45 |
Ishikawa | JAIST | Towards a formal verification of interrupts in TOPPERS/ASP by the separation logic Takashi Nakashima, Shoji Yuen (Nagoya Univ.) SS2011-37 |
We give a formal verification of a fragment of ARM assembly code in TOPPERS/ASP to handle interrupts using the separatio... [more] | SS2011-37 pp.61-66 |
| SS | 2011-06-30 11:30 |
Overseas | Korea Univ. (Seoul) | An Introduction of a Formal Method in PBL: A Case Report Shinya Yamada, Tomohiro Iwamoto, Tsunayuki Shinozawa, Mitsuhide Honda, Ryo Miyashita (Kyushu Univ.), Takashi Iwasaki, Yasuo Inoue (FUJITSU QNET), Keijiro Araki, Shigeru Kusakabe, Yoichi Omori (Kyushu Univ.) SS2011-3 |
In this paper, we report our PBL whose aim is to establish a guideline to introduce formal methods into software develo... [more] |
SS2011-3 pp.11-16 |
| ICSS | 2011-03-25 13:25 |
Tokyo | Suspended | Consideration on hidden-communication channel in the Internet communication device. Tomoki Murota (Univ. of Tokyo), Khin Thida Latt (JAIST), Katsuhiro Horiba (Keio Univ.), Hiroaki Hazeyama (NAIST), Akira Kato (Keio Univ.) ICSS2010-60 |
Since the Internet became the society infrastructure, it is necessary to verify the vulnerability of network equip- men... [more] |
ICSS2010-60 pp.23-28 |
| ISEC, IT, WBS | 2011-03-04 15:45 |
Osaka | Osaka University | Symbolic Criterion for EUC Secure Authentication against Static Adversary Itsuki Suzuki, Maki Yoshida, Toru Fujiwara (Osaka Univ.) IT2010-129 ISEC2010-133 WBS2010-108 |
EUC secure protocol maintains its security even when it is composed and shares public information with arbitrary protoco... [more] | IT2010-129 ISEC2010-133 WBS2010-108 pp.403-410 |
| SWIM | 2010-11-19 15:25 |
Tokyo | Tokai Univ. Takanawa Campus(Tokyo) | Verification of UML Sequence Diagrams with Time Constraints Yoshihiro Yasuda, Yoshiyuki Shinkawa (Ryukoku Univ.) SWIM2010-23 |
Verification of the system specification is usually performed independently from three major different viewpoints, that ... [more] | SWIM2010-23 pp.39-44 |
| MSS | 2010-08-02 14:25 |
Ishikawa | Generating test cases for implementing concurrent systems based on the OTS/CafeOBJ method Takahiro Seino (AIST), Masaki Nakamura (Kanazawa Univ.) CST2010-33 |
In software developments with formal methods, there exists an unavoidable gap between a system description in formal spe... [more] | CST2010-33 pp.7-12 |
|
| VLD | 2010-03-12 13:30 |
Okinawa | Circuit conversion for reducing false negatives on formal verification of sequential circuit Norihiro Ono, Kazuhiro Nakamura, Kazuyoshi Takagi, Naofumi Takagi (Nagoya Univ.) VLD2009-125 |
This paper proposes a reducing method of false negatives by the circuit conversion. We focus that the false negatives oc... [more] | VLD2009-125 pp.157-162 |
|
| MSS | 2009-06-03 16:50 |
Osaka | Setsunan University, Osaka Center | [Invited Talk]
Probabilic Timed CEGAR Atsushi Morishita, Ryota Komagata, Satoshi Yamane (Kanazawa Univ.) CST2009-5 |
In this paper, we present an efficient verification method for probabilic timed automaton. This method based on predicat... [more] | CST2009-5 pp.25-30 |
| SS, KBSE | 2009-05-22 10:00 |
Akita | Akita University | Modeling and Verification of Web Applications Using Formal Approach Kei Homma (Miyagi Univ.), Kaoru Takahashi (Sendai National Coll. of Tech.), Atsushi Togashi (Miyagi Univ.) SS2009-8 KBSE2009-8 |
The number of web applications handling online transaction is increasing, but verification of the correctness of the we... [more] |
SS2009-8 KBSE2009-8 pp.43-48 |
| VLD | 2009-03-12 10:30 |
Okinawa | A Formal Verification Method for On-Chip Programmable Interconnect Takaaki Tagawa, Hiroaki Yoshida, Masahiro Fujita (Univ. of Tokyo) VLD2008-142 |
As the development cost increases, programmable devices such as FPGAs are becoming critically important. A key componen... [more] | VLD2008-142 pp.95-100 |
|
[Return to Top Page]