| 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 # | |
| SS | 2020-03-04 15:10 |
Okinawa | (Cancelled but technical report was issued) |
Transforming Programs with Exclusive Control into Logically Constrained Term Rewrite Systems Misaki Kojima, Naoki Nishida, Yutaka Matsubara, Masahiko Sakai (Nagoya Univ.)  SS2019-46 |
To apply Logically Constrained Term Rewrite Systems (LCTRSs, for short) to program verification, a previous work targets... [more] | SS2019-46 pp.31-36 |
| MSS, NLP (Joint) |
2018-03-13 14:55 |
Osaka | Deductive Verification of real-time safety properties for embedded assembly program using theorem prover Princess Naoki Odajima (Kanazawa Univ.), Gakuhi Fukuda (Kanazawa Nishikigaoka), Satoshi Yamane (Kanazawa Univ.) MSS2017-84 |
It is important to verify both the correctness and real-time properties for embedded systems. In this paper, we propos... [more] |
MSS2017-84 pp.35-40 |
|
| ICTSSL, CAS | 2018-01-26 10:00 |
Tokyo | Kikai-Shinko-Kaikan Bldg. | On a Development and introduction of Program Logic Verification Method based on Japanese Patent PA4958574 Hideaki Okazaki (SIT), Kunio Takai (TB) CAS2017-122 ICTSSL2017-49 |
In this report, we introduce the program logic verification method, from the viewpoint of mathematical dynamical systems... [more] | CAS2017-122 ICTSSL2017-49 pp.63-68 |
| SIP, CAS, MSS, VLD | 2017-06-20 09:30 |
Niigata | Niigata University, Ikarashi Campus | Deductive Verification Method of real-time safety properties for embedded assembly program
-- □≦TIME q = □(q∧(time≦TIME)) -- Satoshi Yamane (Kanazawa Univ.) CAS2017-12 VLD2017-15 SIP2017-36 MSS2017-12 |
It is important to verify both the correctness and real-time properties for embedded systems. In this paper, we propos... [more] |
CAS2017-12 VLD2017-15 SIP2017-36 MSS2017-12 pp.59-64 |
| SS | 2016-03-10 11:15 |
Okinawa | Program Verification Using Non-linear Loop Invariants Generated by Partially Applying an Extended Farkas' Lemma Makishi Yanagisawa, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) SS2015-81 |
To generate loop invariants, methods that, using Farkas' lemma, convert verification formulas obtained from a given temp... [more] | SS2015-81 pp.31-36 |
|
| MSS, CAS, IPSJ-AL [detail] | 2015-11-20 14:20 |
Kagoshima | Ibusuki CityHall | Program syntesis from execution traces andt its program verification of distributed algorithms Satoshi Yamane (Kanazawa Univ.) CAS2015-50 MSS2015-24 |
Distributed algorithms are executed on distributed systems such as cloud computing and P2P. It is important to verify ... [more] |
CAS2015-50 MSS2015-24 pp.35-40 |
| KBSE | 2012-11-22 11:25 |
Ishikawa | Kanazawa University | SMT-based Bounded Model Checking for Assembly program Junpei Kobashi, Atsushi Takeshita, Satoshi Yamane (Kanazawa Univ.) KBSE2012-41 |
In this paper, we state property verification by Bounded Model Checking using SMT solver for register level model of ass... [more] | KBSE2012-41 pp.19-24 |
[Return to Top Page]