| 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 # | |
| KBSE | 2024-03-15 13:20 |
Okinawa | Okinawa Prefectual General Welfare Center (Primary: On-site, Secondary: Online) |
On Improvement of Variability Model Division Method Tomoji Kishi (Waseda Univ.)  KBSE2023-87 |
The analysis and verification of variability models are often based on logic, but the number of configurations of a vari... [more] | KBSE2023-87 pp.120-125 |
| RCC, ISEC, IT, WBS | 2024-03-14 15:30 |
Osaka | Osaka Univ. (Suita Campus) | Research Directions in Formal Verification of Transport Layer Security Protocols Hideki Sakurada (NTT/Kyushu Univ.), Kouichi Sakurai (Kyushu Univ./ATR) IT2023-121 ISEC2023-120 WBS2023-109 RCC2023-103 |
The TLS protocol is used to secure communications between web servers and clients, and is essential for security: it all... [more] | IT2023-121 ISEC2023-120 WBS2023-109 RCC2023-103 pp.287-293 |
| VLD, HWS, ICD | 2024-03-02 12:05 |
Okinawa | (Primary: On-site, Secondary: Online) |
A Study on formal verification of GF(2^m) arithmetic circuits including states Kazuho Sakoda (SCU/Kobe Univ.), Yasuyoshi Uemura (SCU), Naofumi Homma (Tohoku Univ.) VLD2023-140 HWS2023-100 ICD2023-129 |
This paper describes a formal verification method for arithmetic circuits based on computer algebra. Conventional method... [more] | VLD2023-140 HWS2023-100 ICD2023-129 pp.215-220 |
| KBSE, SC | 2023-11-17 15:30 |
Miyagi | Sento Kaikan | Variability Model Division for Scalability Improvement Tomoji Kishi (WU) KBSE2023-37 SC2023-20 |
Variability models have been used for logic-based analysis and verification, but the number of variations is combinatori... [more] | KBSE2023-37 SC2023-20 pp.31-36 |
| KBSE | 2023-03-17 14:35 |
Hiroshima | JMS ASTERPLAZA (Primary: On-site, Secondary: Online) |
Development of Co-Analysis Support Tool by Linking Simulink and SMT Solver Engielista Anak Norman, Yoshikazu Ueda (Ibaraki Univ.) KBSE2022-67 |
In order to target various models in co-analysis, it is necessary to be able to select the SMT solver according to the c... [more] | KBSE2022-67 pp.79-84 |
| ITS, IEE-ITS | 2021-03-15 15:05 |
Online | Online | Model Checking-Based Verification of Token-Based Traffic Control for Roundabouts Tatsuhiro Tsuchiya (Osaka Univ.), Satoshi Otsuka (Hitachi) ITS2020-43 |
This paper reports the results of model checking-based verification of a traffic control mechanism for roundabouts. This... [more] | ITS2020-43 pp.41-44 |
| NS, ICM, CQ, NV (Joint) |
2020-11-27 11:45 |
Online | Online | A Proposal of Framework for Authentication Systems and Verification Method Motoshi Horii, Toshihiro Shimizu (Fujitsu Lab.), Satoshi Imai (Fujitsu) CQ2020-58 |
With the digitization of various procedures, various security incidents have been occurring frequently. To prevent the o... [more] | CQ2020-58 pp.62-65 |
| HWS, VLD [detail] | 2020-03-04 10:30 |
Okinawa | Okinawa Ken Seinen Kaikan (Cancelled but technical report was issued) |
An EVBDD-based Design Verification for Elementary Function Generators Hiroto Fukuhara, Shinobu Nagayama, Masato Inagi, Shin'ichi Wakabayashi (HCU) VLD2019-96 HWS2019-69 |
This paper proposes a design verification based on edge-valued binary decision diagrams (EVBDDs) for elementary functio... [more] |
VLD2019-96 HWS2019-69 pp.13-18 |
| ISEC, SITE, ICSS, EMM, HWS, BioX, IPSJ-CSEC, IPSJ-SPT [detail] | 2019-07-23 13:10 |
Kochi | Kochi University of Technology | A Formal Approach to Verifying Trojan-freeness of Cryptographic Circuits Based on Galois-Field Arithmetic Akira Ito, Rei Ueno, Naofumi Homma (Tohoku Univ.) ISEC2019-26 SITE2019-20 BioX2019-18 HWS2019-21 ICSS2019-24 EMM2019-29 |
This paper proposes a formal method for verifying whether Hardware Trojan (HT) exists or not (i.e., HT-freeness) in cryp... [more] | ISEC2019-26 SITE2019-20 BioX2019-18 HWS2019-21 ICSS2019-24 EMM2019-29 pp.133-138 |
| SS | 2019-03-04 17:10 |
Okinawa | Formal STAMP Modelling toward Safety Verification of Hybrid Systems Mitsuaki Tsuji, Toshinori Takai (NAIST), Masafumi Katahira, Naoki Ishihama (JAXA), Kazuki Kakimoto, Hajimu Iida (NAIST) SS2018-67 |
Safety-critical systems, for example, autonomous vehicles and space systems, are required to be safe and reliable. Recen... [more] | SS2018-67 pp.91-96 |
|
| MSS, CAS, IPSJ-AL [detail] | 2018-11-13 15:15 |
Shizuoka | On formal verification of mathematical programming models by algebraic specifications Masaki Nakamura, Kazutoshi Sakakibara (Toyama Pref. Univ.) CAS2018-76 MSS2018-52 |
To apply a solver for optimization problems, we need to formalize a problem into a form acceptable by the solver. In th... [more] |
CAS2018-76 MSS2018-52 pp.127-130 |
|
| VLD | 2016-02-29 13:30 |
Okinawa | Okinawa Seinen Kaikan | Tool Support for Verifying Large Scale Hardware Design with Verilog-HDL Yuta Morimitsu, Tomoyuki Yokogawa (Okayama Prefectural Univ.), Masafumi Kondo, Hisashi Miyazaki (Kawasaki Univ. of Medical Welfare), Yoichiro Sato, Kazutami Arimoto (Okayama Prefectural Univ.), Norihiro Yoshida (Nagoya Univ.) VLD2015-111 |
In this paper, we developed a tool supporting formal verification of large scale hardware design described by Verilog-HD... [more] | VLD2015-111 pp.1-6 |
| KBSE, SS, IPSJ-SE [detail] | 2015-07-24 09:00 |
Hokkaido | A Study on a Formal Verification Method Using Atelier-B Ryota Yamamoto, Shuichiro Yamamoto (Nagoya Univ.) SS2015-29 KBSE2015-22 |
In this paper, we try to evaluate a formal verification method using Atelier-B, a delopment tool for B-method. To enhanc... [more] | SS2015-29 KBSE2015-22 pp.143-148 |
|
| QIT (2nd) |
2015-05-25 13:20 |
Osaka | Osaka University | [Poster Presentation]
Formal Verification of Robertson-type Uncertainty Relation Takaaki Masuhara, Toru Kuriyama, Masakazu Yoshida, Jun Cheng (Doshisha Univ.) |
Formal verification using interactive theorem provers have been noticed as a method of verification of proofs that are t... [more] | |
| MSS | 2015-03-06 10:25 |
Ishikawa | IT Business Plaza Musashi | Development of SMT-based model checker for assembly cords using interrupts reduction technique Junpei Kobashi, Atsushi Takeshita, Satoshi Yamane, Kohei Sakurai (Kanazawa Univ.) MSS2014-100 |
Recently, embedded software has properties dependent on hardware (direct operation of address spaces, memory mapped I/O,... [more] | MSS2014-100 pp.53-58 |
| VLD, DC, IPSJ-SLDM, CPSY, RECONF, ICD, CPM (Joint) [detail] |
2014-11-26 10:45 |
Oita | B-ConPlaza | A hardware description method and sematics providing a timing constrant Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) VLD2014-82 DC2014-36 |
Formal verification methods are wide-spreading due to its mathmatical rigorousaspect, although they limited to synchroun... [more] | VLD2014-82 DC2014-36 pp.81-86 |
| RECONF | 2014-09-19 14:40 |
Hiroshima | Formal Verification System of Multi-clock Synchronous Circuits on Multimodal Logic Shunji Nishimura, Motoki Amagasaki, Toshinori Sueyoshi (Kumamoto Univ.) RECONF2014-33 |
Regardless of wide using of a formal verification methods, almost all of the methods limited to single-clock synchrounou... [more] | RECONF2014-33 pp.93-98 |
|
| SC, IPSJ-UBI | 2014-07-28 10:00 |
Tokyo | National Institute of Informatics | Formal verification for service composition of formaly verified services using different mechanisms Kazuhiro Funakoshi, Shigeru Hosono (NEC) SC2014-6 |
This presentation describes a case study to generate models on proof assistant Coq with input of multiple Web services' ... [more] | SC2014-6 pp.49-54 |
| SS | 2014-03-11 10:30 |
Okinawa | Tenbusu Naha | Generation and Verification of Decision Table using SAT Solver Shinji Itoh, Naoto Sato, Hidetaka Kondoh, Kunihiko Miyazaki, Hiroki Mori, Makoto Kimura, Kiyoshi Yamaguchi (Hitachi) SS2013-73 |
Use of a decision table is an effective method to prevent defects of combination patterns of conditions. However, it is ... [more] | SS2013-73 pp.7-11 |
| SS | 2014-03-11 11:30 |
Okinawa | Tenbusu Naha | Formal Verification Technique for Consistency Checking between equals and hashCode methods in Java Hiroaki Shimba, Hiroki Onoue, Kozo Okano, Shinji Kusumoto (Osaka Univ.) SS2013-75 |
Java classes must observe constraints on ``hashCode'' methods as well as ``equals'' methods, in order to behave correctl... [more] | SS2013-75 pp.19-24 |
[Return to Top Page]