| 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 # | |
| MSS, SS | 2015-01-27 12:55 |
Tottori | Towards Security Analysis based on Traceability Hirokazu Yatsu (Kyushu Univ.), Masaru Matsunami (SDNA), Toshimi Sawada (Thinker's craft house), Takahiro Ando, Kenji Hisazumi (Kyushu Univ.), Kong Weiqiang (DLUT), Akira Fukuda (Kyushu Univ.) |
Usually, security analysis is mainly done at the implementation phase of system development. In this paper, we propose a... [more] | ||
| IA, IN (Joint) |
2014-12-19 11:30 |
Hiroshima | Hiroshima City University | The Architecture of Delay Tolerant Networking over the Internet Masataka Ohta (Tokyo Inst. of Tech.)  IA2014-77 |
Not to mention Interplanetary communication, UUCP network is DTN, from history of which, we can recognize how DTN over t... [more] | IA2014-77 pp.49-50 |
| SS | 2014-03-11 10:00 |
Okinawa | Tenbusu Naha | An Extension of Alloy with Time Constraints Ryota Kuroita, Shoji Yuen (Nagoya Univ.) SS2013-72 |
This paper proposes an extension of Alloy, called Alloy-R, with constraints for reals in purpose of specifying time-dep... [more] | SS2013-72 pp.1-6 |
| 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 |
| EMD | 2014-01-31 14:50 |
Tokyo | A Study of Thermal Deformation of box type resin part in Reflow Process Masayuki Tamura, Toshiyuki Shimoda (JAE) EMD2013-139 |
LCP is used many of Insulator(INS) materials. Resins of LCP have the big anisotropy of the coefficient of thermal expans... [more] | EMD2013-139 pp.17-22 |
|
| 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 |
|
| MSS, SS | 2013-03-07 11:40 |
Fukuoka | Shikanoshima | On Composing the Simplex Method and Gomory Cut for Deriving Integer Assignments Masaaki Fushimi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) MSS2012-78 SS2012-78 |
The simplex method is one of the methods to derive rational assignments from linear constraints on ratiolals. It is know... [more] | MSS2012-78 SS2012-78 pp.109-114 |
| 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 |
| 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 |
| MSS, CAS | 2012-11-02 13:30 |
Iwate | Iwate University | Scheduling and Resource Assignment of Periodic Tasks in Computer Networks Using an SMT Solver Yuya Sakai, Toshimitsu Ushio (Osaka Univ.) CAS2012-62 MSS2012-42 |
It is important in computer networks to assign each task to a computer in order to have scheduling without deadline miss... [more] | CAS2012-62 MSS2012-42 pp.71-74 |
| VLD, CAS, MSS, SIP | 2012-07-02 13:00 |
Kyoto | Kyoto Research Park | Verification of embedded software in Assembly code by SMT prover Atsushi Takeshita, Junpei Kobashi, Satoshi Yamane (Kanazawa Univ.) CAS2012-7 VLD2012-17 SIP2012-39 MSS2012-7 |
We propose the technique of Bounded Model Checking(BMC) for embedded assembly program. We use SMT solver for BMC. We als... [more] | CAS2012-7 VLD2012-17 SIP2012-39 MSS2012-7 pp.37-42 |
| IA, SITE, IPSJ-IOT [detail] | 2012-03-15 15:25 |
Hokkaido | Hokkaido Univ. | A study of implementation for A 1-Round Almost Secure Message Transmission Protocol Tomoya Kuriyama (Kanagawa Univ.), Kazuhiro Suzuki (Kochi Univ.), Hirotsugu Kinoshita (Kanagawa Univ.), Tetsuya Morizumi (Toyo Networks & System Integration Co , Ltd.) SITE2011-36 IA2011-86 |
A public key cryptosystem needs a trusted third party that proves the legitimacy of public keys. However,an n-channel s... [more] |
SITE2011-36 IA2011-86 pp.37-42 |
| SS | 2012-03-13 13:55 |
Okinawa | Tenbusu-Naha | Automatic derivation of test cases for Java using an SMT solver and a PDG generator. Yukihiro Sasaki, Kazuki Kobayashi, Kozo Okano, Shinji Kusumoto (Osaka Univ) SS2011-66 |
Assertions and Design by Contract play important roles for program understanding and program verification. In order to g... [more] | SS2011-66 pp.55-60 |
| SS, MSS | 2012-01-26 11:15 |
Kochi | Kochi City Culture-Plaza Cul-Port | Architectual Point Mapping for Bidirectional Traceability between Design and Code Naoyasu Ubayashi, Yasutaka Kamei (Kyushu Univ.) MSS2011-57 SS2011-42 |
Well-designed architecture leads to high-quality systems. However, it is not easy to design architecture reflecting the... [more] |
MSS2011-57 SS2011-42 pp.15-20 |
| VLD, CPSY, RECONF, IPSJ-SLDM [detail] | 2012-01-25 13:55 |
Kanagawa | Hiyoshi Campus, Keio University | An IPC Control Mechanism for Real-Time Processing on a Prioritized SMT Processor Kensuke Kaneda, Kohei Matsumoto, Nobuyuki Yamasaki (Keio Univ) VLD2011-97 CPSY2011-60 RECONF2011-56 |
Although the SMT processor which performs two or more threads simultaneously can improve total throughput, the execution... [more] | VLD2011-97 CPSY2011-60 RECONF2011-56 pp.37-42 |
| VLD, CPSY, RECONF, IPSJ-SLDM [detail] | 2012-01-25 14:20 |
Kanagawa | Hiyoshi Campus, Keio University | Extension of ITRON Specification OS for Multithreaded Processors Rikuhei Ueda, Kei Fujii, Hiroyuki Chishiro, Hiroki Matsutani, Nobuyuki Yamasaki (Keio Univ.) VLD2011-98 CPSY2011-61 RECONF2011-57 |
Recent advances in embedded systems have demanded high-performance under real-time constraints.Responsive Multithreaded ... [more] | VLD2011-98 CPSY2011-61 RECONF2011-57 pp.43-48 |
| DC | 2011-10-20 11:00 |
Tokyo | K-induction-based model checking of concurrent systems with unbounded integer variables Hiroyuki Inoue, Tatsuhiro Tsuchiya, Tohru Kikuno (Osaka Univ.) DC2011-20 |
We discuss k-induction-based model checking that uses a Satisfiability Modulo Theories (SMT) solver. The state space of ... [more] | DC2011-20 pp.1-5 |
|
| SDM | 2011-10-21 09:50 |
Miyagi | Tohoku Univ. (Niche) | Channel strain measurements in 32nm-node CMOSFETs Munehisa Takei, Hiroki Hashiguchi, Takuya Yamaguchi, Daisuke Kosemura, Kohki Nagata, Atsushi Ogura (Meiji Univ.) SDM2011-104 |
We performed strain analyses for 32-nm-node MPU by Raman measurements in conjunction with TEM observation. The channel s... [more] | SDM2011-104 pp.43-48 |
| SS | 2010-10-15 11:00 |
Iwate | Iwate Prefectural Univ. | On DPLL Transition Systems Modulo Equational Theories Tatsuya Baba, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) SS2010-36 |
SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so ... [more] | SS2010-36 pp.49-54 |
| SS | 2010-03-08 11:40 |
Kagoshima | Kagoshima Univ. | On a Combination Method of Decision Procedures for Theories Sharing Common Symbols Koji Iwanuma (Univ. of Yamanashi) SS2009-67 |
The Nelson-Oppen method is a well-known general framework for combining decision procedures into a single decision proce... [more] | SS2009-67 pp.115-120 |
[Return to Top Page]