| 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-14 14:10 |
Okinawa | Okinawa Prefectual General Welfare Center (Primary: On-site, Secondary: Online) |
Applying Model Checking to Ethical Judgments Yoshitaka Aoki, Yotaro Nakayama (BIPROGY)  KBSE2023-73 |
(To be available after the conference date) [more] | KBSE2023-73 pp.49-54 |
| KBSE | 2023-03-17 10:40 |
Hiroshima | JMS ASTERPLAZA (Primary: On-site, Secondary: Online) |
Verification of Interaction between Functions in FRAM using Model Checking Yoshitaka Aoki (BIPROGY), Kenji Hisazumi (Shibaura Inst. of Tech.) KBSE2022-62 |
Analysis of FRAM models tends to rely on the domain knowledge of analysts, and it is difficult for anyone to evaluate co... [more] | KBSE2022-62 pp.49-54 |
| KBSE | 2023-03-17 12:50 |
Hiroshima | JMS ASTERPLAZA (Primary: On-site, Secondary: Online) |
On Family-based Model Checking based on Probabilistic Model Checker Tomoji Kishi (Waseda Univ) KBSE2022-64 |
Family-based model checking is a technique to verify the properties of multiple product variations at once by performing... [more] | KBSE2022-64 pp.61-66 |
| SS | 2023-03-15 09:55 |
Okinawa | (Primary: On-site, Secondary: Online) |
Regularity Preservation Property of Data Tree Rewrite Systems
-- A Subclass Decomposable into Monadic Normal Form -- Yuto Sakao, Hiroyuki Seki (Nagoya Univ.) SS2022-62 |
Let $T$ be a transformation over a class $mathcal{L}$ of languages. If for any regular language $L in mathcal{L}$, $T^*(... [more] | SS2022-62 pp.91-96 |
| SS, IPSJ-SE, KBSE [detail] | 2022-07-29 13:00 |
Hokkaido | Hokkaido-Jichiro-Kaikan (Sapporo) (Primary: On-site, Secondary: Online) |
Verification of Implementable Timed Automata via Satisfiability Checking Seiichiro Tachi, Shoji Yuen (Nagoya Univ.) SS2022-9 KBSE2022-19 |
We present a technique for bounded model-checking the reachability in timed automata with implementability assuming that... [more] | SS2022-9 KBSE2022-19 pp.49-54 |
| MSS, NLP | 2022-03-28 10:05 |
Online | Online | Formal Verification of Control Policy of Elevator Systems using Statistical Model Checking Yuki Kitahara, Masaki Nakamura, Kazutoshi Sakakibara (Toyama Pref. Univ.) MSS2021-57 NLP2021-128 |
When designing an elevator system, efficient control laws can be expected to be obtained by considering the probability ... [more] | MSS2021-57 NLP2021-128 pp.13-18 |
| SS, DC | 2021-10-19 15:25 |
Online | Online | A Subclass of Mu-Calculus with the Freeze Quantifier Equivalent to Register Automata Akira Onishi, Ryoma Senda (Nagoya Univ.), Yoshiaki Takata (KUT), Hiroyuki Seki (Nagoya Univ.) SS2021-17 DC2021-22 |
Register automaton (abbreviated as RA) is an extension of finite automaton by adding registers storing data values. RA ... [more] |
SS2021-17 DC2021-22 pp.23-28 |
| 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 |
| SS | 2021-03-03 10:25 |
Online | Online | A Subclass of LTL with the Freeze Quantifier Translatable into Register Automata Akira Onishi, Ryoma Senda (Nagoya Univ.), Yoshiaki Takata (KUT), Hiroyuki Seki (Nagoya Univ.) SS2020-29 |
Register automaton (abbreviated as RA) is an extension of finite automaton by adding registers storing data values. RA ... [more] |
SS2020-29 pp.7-12 |
| SS | 2021-03-04 13:25 |
Online | Online | Generating Exhaustive Counterexample and Path Constraint with Software Analysis Workbench and Symbolic PathFinder Rin Karashima, Shinpei Ogata, Kozo Okano (Shinshu Univ.) SS2020-41 |
Software Analysis Workbench (SAW) generates models from JVM bytecode by symbolic execution. Users can perform model che... [more] |
SS2020-41 pp.78-83 |
| DC, SS | 2020-10-19 13:25 |
Online | Online | LTL Model Checking for Register Pushdown Systems Ryoma Senda (Nagoya Univ.), Yoshiaki Takata (KUT), Hiroyuki Seki (Nagoya Univ.) SS2020-6 DC2020-23 |
A pushdown system (PDS) is known as an abstract model of recursive programs. For PDS, model checking methods have been ... [more] |
SS2020-6 DC2020-23 pp.7-12 |
| KBSE | 2020-03-06 13:30 |
Okinawa | Tenbusu-Naha (Cancelled but technical report was issued) |
A Method to Analyze the Proximate States to Hazards Based-on State Transition System for Supporting Safety Analysis Yusuke Suzuki, Shinpei Ogata, Yutaro Ohike (Shinshu Univ.), Yoshitaka Aoki (Nihon Unisys), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi, Kozo Okano (Shinshu Univ.) KBSE2019-47 |
STAMP (System-Theoretic Accident Model and Processes）/STPA (System-Theoretic Process Analysis) supports system developer... [more] | KBSE2019-47 pp.7-12 |
| SS | 2020-03-05 12:05 |
Okinawa | (Cancelled but technical report was issued) |
An Approach of Deriving Hazard Transition Series by Cooperation of STAMP/STPA and Model Checking Pan Yang, Kozo Okano, Shinpei Ogata (Shinshu Univ.), Keishi Okamoto (Sendai National College of Tech.) SS2019-56 |
The demand for research on the hazard analysis of information systems and the construction of countermeasures have been ... [more] | SS2019-56 pp.93-98 |
| ICSS, IPSJ-SPT | 2020-03-03 11:00 |
Okinawa | Okinawa-Ken-Seinen-Kaikan (Cancelled but technical report was issued) |
Model checking RNNs with modal μ-calculus Tatsuhiro Aoshima, Toshinori Usui (NTT) ICSS2019-88 |
Machine learning models have been applied to many cyber-physical systems such as self-driving cars, robotics, and factor... [more] | ICSS2019-88 pp.119-124 |
| KBSE, SC | 2019-11-08 11:30 |
Nagano | Shinshu University | A Method to Analyze NuSMV Counterexamples for Defect Cause Analysis Yutaro Ohike, Shinpei Ogata (Shinshu Univ.), Yoshitaka Aoki (Nihon Unisys, Ltd.), Hiroyuki Nakagawa (Osaka Univ.), Kazuki Kobayashi, Kozo Okano (Shinshu Univ.) KBSE2019-24 SC2019-21 |
Many state variables that are defined in a model may appear as conditional expressions in one specification on model che... [more] | KBSE2019-24 SC2019-21 pp.7-12 |
| SWIM, KBSE | 2019-05-25 09:45 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | A Proposal of FRAM Support Method using Probabilistic Model Checker Yoshitaka Aoki (NUL), Shinpei Ogata (Shinshu Univ) KBSE2019-8 SWIM2019-8 |
FRAM (Functional Resonance Analysis Method) is an analysis method to analyze and model a complex technical system. The F... [more] | KBSE2019-8 SWIM2019-8 pp.49-56 |
| NLP, MSS (Joint) |
2019-03-15 15:55 |
Fukui | Bunkyo Camp., Univ. of Fukui | A derivation of weighted transition system for Simulink models from simulation results Ryota Owaki (Nagoya Univ), Shoji Yuen (Nagooya Univ) MSS2018-95 |
We propose a method to generate a symbolic weighted transition system from a Simulink model description. Continuous va... [more] |
MSS2018-95 pp.75-80 |
| SS | 2019-03-04 10:15 |
Okinawa | Statistical model checking of hybrid systems with Acumen Kosuke Inoue, Daisuke Ishii (Fukui Univ.) SS2018-54 |
An integrated tool for modeling, simulation and verification is useful for developing reliable continuous/discrete hybri... [more] | SS2018-54 pp.13-18 |
|
| SS | 2019-03-05 15:25 |
Okinawa | Automatic Repair of Conditional Expressions for Functional Programs by Using Counterexamples Ken Matsui, Ryosuke Sato, Naoyasu Ubayashi, Yasutaka Kamei (Kyushu Univ.) SS2018-80 |
In software development, manual bug fixing consumes much time and effort. Therefore, automated program repair methods ha... [more] | SS2018-80 pp.169-174 |
|
| MSS, CAS, IPSJ-AL [detail] | 2018-11-13 14:50 |
Shizuoka | Process mining approach for the conformance checking of discrete-event simulation model Kenji Uehara, Kunihiko Hiraishi (JAIST) CAS2018-75 MSS2018-51 |
Discrete-event simulation is an effective method to reproduce the target system behavior and to investigate its mechanis... [more] | CAS2018-75 MSS2018-51 pp.121-126 |
|
[Return to Top Page]