| Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
| SS, KBSE |
2006-10-26
13:40 |
Ehime |
Ehime University |
Approach to Software Verification Based on Transforming from Procedural Programs to Rewrite Systems
Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
In the field of term rewriting, inductionless induction and rewriting
induction have been widely studied as methods for... [more] |
SS2006-41 KBSE2006-17
pp.7-12 |
| SS, KBSE |
2006-10-26
14:05 |
Ehime |
Ehime University |
Security Analysis of Information Flow for An Object-Oriented Language with Exception Handling
Sho Kurokawa, Hiroaki Kuwabara (Nagoya Univ), Shinichiro Yamamoto (Aichi Prefectural Univ), Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ) |
In this paper, we propose a type system for verifying that secret data don't leak from an object-oriented program with e... [more] |
SS2006-42 KBSE2006-18
pp.13-18 |
| SS, KBSE |
2006-10-26
16:15 |
Ehime |
Ehime University |
Example programs generated by GeneSys and proposal of Introduction rule
Satoru Kondo, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) |
Program Generation System GeneSys is a method for generating executable programs from specifications described in first-... [more] |
SS2006-46 KBSE2006-22
pp.37-42 |
| SS |
2006-06-22
14:00 |
Okayama |
|
Transformation of Equational Rewriting Systems for Removing some Equations
Koichi Miura, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) |
In equational rewriting, which is rewriting modulo equations, the set of all direct successors from a given term is in g... [more] |
SS2006-14
pp.7-12 |
| SS |
2006-06-22
14:45 |
Okayama |
|
Usable Rules and Labeling Product-Typed Term for Dependency Pair Method in Simply-Typed Term Rewriting Systems
Takahiro Sakurai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) |
[more] |
SS2006-15
pp.13-18 |
| SS |
2006-04-20
16:10 |
Niigata |
Niigata Univ., Igarashi Campus |
Proving Termination of Higher-Order Rewrite Systems based on Strongly Computable Dependency Pair Method
Yasuo Isogai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) |
The higher-order rewrite systems (HRS for short) are a computation model of functional programming languages, and hence ... [more] |
SS2006-6
pp.31-36 |
| SS |
2006-02-02
16:45 |
Fukuoka |
Fukuoka Laboratory for Emerging and Enabling Technology of SoC |
Secrecy Verification of Spi Calculus based on Term Regular Expressions
Yoshihiko Tashiro, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) |
[more] |
SS2005-82
pp.35-40 |
| SS |
2006-02-03
10:30 |
Fukuoka |
Fukuoka Laboratory for Emerging and Enabling Technology of SoC |
Lexicographic Path Ordering for Proving Termination of Functional Programs
Yumi Hoshino, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) |
Term rewriting system is a computational model of functional programs, and termination is one of the important propertie... [more] |
SS2005-85
pp.13-18 |
| COMP |
2005-12-22
11:25 |
Tokushima |
The University of Tokushima |
Decidability of Termination for Left-Linear Shallow Term Rewriting Systems and Related
Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
In this paper, we show that the termination is decidable for left-linear shallow term rewriting systems. The decision pr... [more] |
COMP2005-50
pp.9-13 |
| SS |
2005-12-19
14:30 |
Kochi |
Kochi Women's University |
Secrecy Verification by Transforming Cryptographic Protocol Descriptions to Coloured Petri Nets
Daisuke Okuya, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) |
Verification of the safety of cryptographic protocols can be
mechanized by reducing the safety to the reachability of C... [more] |
SS2005-58
pp.19-24 |
| SS |
2005-12-20
11:15 |
Kochi |
Kochi Women's University |
Type Judgement System for Communication Error in Distributed JoinJAVA Programs
Masaki Saeki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) |
The distributed JoinJAVA is the Join-Calculus extended by adding JAVA
fragments as sequential processes. It enables us ... [more] |
SS2005-67
pp.25-30 |
| SS |
2005-10-13
16:15 |
Saitama |
Jumonji University |
On Completeness of Outermost Strategy for Overlapping TRSs
Atsushi Iwata, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
Strategies in term rewriting systems (TRSs) indicate a position of a given term to be reduced. Since a term generally ha... [more] |
SS2005-46
pp.39-44 |
| SS |
2005-08-04
14:00 |
Hokkaido |
Otaru Univ. of commerce, Room 407 |
Decidability of Termination for Semi-Constructor Term Rewriting Systems
Yi Wang, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
[more] |
SS2005-26
pp.13-18 |
| SS |
2005-06-24
10:45 |
Nagano |
Shinshu Univ. Ohta-Kokusai-Kinenkan |
On Proving Termination of Simply-Typed Term Rewriting Systems Based on Strong Computability
Keiichirou Kusakari, Takahiro Sakurai, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) |
Terminating functional programs are safe in execution, and valuable because their reduction relations are suitable for i... [more] |
SS2005-21
pp.19-24 |
| SS |
2005-06-24
11:15 |
Nagano |
Shinshu Univ. Ohta-Kokusai-Kinenkan |
Programming Method in Obfuscated Language Malbolge
Hisashi Iizawa, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) |
Malbolge is an obfuscated (esoteric) programming language, which is designed to be difficult to program in. In this pape... [more] |
SS2005-22
pp.25-30 |
| SS |
2005-06-24
11:45 |
Nagano |
Shinshu Univ. Ohta-Kokusai-Kinenkan |
Dependency Graph Method for Proving Termination of Narrowing
Koichi Miura, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
Term rewriting systems with extra variables (called EV-TRSs) has an ability to represent inverse-computation programs, a... [more] |
SS2005-23
pp.31-36 |
| SS |
2005-04-22
12:35 |
Wakayama |
|
JavaScript Type Checker based on Model Generation Theorem Prover
Hirotaka Ohkubo, Shinichiro Yamamoto (Aichi Pref. Univ.), Toshiki Sakabe (Nagoya Univ.), Yasuyoshi Inagaki (Aichi Pref. Univ.) |
[more] |
SS2005-11
pp.25-30 |
| SS |
2004-11-25
17:00 |
Yamanashi |
Univ. of Yamanashi, Kofu(Takeda) Campus |
Simulating Fusion Transformation by Program-Generation Transformation
Masanori Nagashima, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) |
Program-Generation Transformation $\mathcal{GS}$ based on first-order logic with equality can handle specifications with... [more] |
SS2004-33
pp.43-48 |
| SS |
2004-08-02
16:45 |
Hokkaido |
Future University Hakodate |
Front-end for JavaScript Type Checker based on Model Generation Theorem Prover
Hirotaka Ohkubo, Shinichiro Yamamoto (Aichi Pref. Univ.), Toshiki Sakabe (Nagoya Univ.), Yasuyoshi Inagaki (Aichi Pref. Univ.) |
[more] |
SS2004-13
pp.41-46 |
| SS |
2004-08-03
13:00 |
Hokkaido |
Future University Hakodate |
On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems
Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) |
Transformations from conditional term rewriting systems (CTRSs)
over (original) signatures
into term rewriting systems... [more] |
SS2004-18
pp.25-30 |