Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 181 - 200 of about 249 ／ All the affair displays >>

Approach to Procedural-program Verification Based on Implicit Induction of Constrained Term Rewriting Reviewed

Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe

IPSJ Transactions on Programming, Vol. 1 ( 2 ) page： 100-121 2008.9

Language：Japanese Publishing type：Research paper (scientific journal)

In the field of procedural programming, several verification methods based
on model checking or Hoare logic have been proposed. On the other hand,
in the field of term rewriting, implicit induction and rewriting induction have
been widely studied as methods for proving inductive theorems. In this paper,
we try to take advantages of methods for proving inductive theorems in verifying
procedural functions written in a "while" language with natural number
type. More precisely, we propose a transformation from procedural programs to
constrained term rewriting systems whose constraints are in Presburger arithmetic,
and show that the transformation reduces the equivalence of procedural
programs to that of functions in rewrite systems. By verifying the equivalence
between rewrite systems, we verify the equivalence between the corresponding
procedural functions. To establish this approach, we extend Critical Pair
Theorem and the basic completion procedure for constrained systems.

Completion as Post-Process in Program Inversion of Injective Functions Reviewed

Naoki Nishida and Masahiko Sakai

Proceedings of the 8th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'08) page： 61-75 2008.7

A Reduction Order for Orienting Equations in Theorem Proving of Constrained TRSs

Naoki Nishida, Tsubasa Sakata, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe

IEICE Technical Report SS2008-20 Vol. 108 ( 173 ) page： 43-48 2008.7

On Rewriting Induction for Presburger-Constrained Term Rewriting Systems

Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari

IEICE Technical Report SS2008-1 Vol. 108 ( 64 ) page： 1-6 2008.5

A Type System for Analyzing Secure Information Flow in Object-Oriented Programs with Exception Handling Reviewed

Sho Kurokawa, Hiroaki Kuwabara, Shinichirou Yamamoto, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

The IEICE Transactions on Information and Systems Vol. J91-D ( 3 ) page： 757-770 2008.3

Approach to Procedural-Program Verification Based on Implicit Induction

Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe

the 68th Workshop on IPSJ Special Interest Group on Programming. page： 1-22 2008.3

A Sufficient Condition for Termination of Transformations from Equations to Rewrite Rules

Kiyotaka Mizuno, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari

IEICE Technical Report SS2007-61 Vol. 107 ( 505 ) page： 25-30 2008.3

Error Detection with Soft Typing for Dynamically Typed Languages

Akihisa Yamada, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

IEICE Technical Report SS2007-58 Vol. 107 ( 505 ) page： 7-12 2008.3

Extending program-generation system GeneSys for allowing negation in equational specifications

Satoru Kondo, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

IEICE Technical Report SS2007-45 Vol. 107 ( 392 ) page： 43-48 2007.12

A Tool for Designing Sudoku Problems by Interactive Fill-in Approach

Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

IEICE Technical Report SS2007-50 Vol. 107 ( 392 ) page： 73-78 2007.12

Proving Non-termination of Logic Programs by Detecting Loops in Derivation Trees

Tomohiro Mizutani, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

IEICE Technical Report SS2007-30 Vol. 107 ( 275 ) page： 1-6 2007.10

Finding Magic Squares Based on CNF Encoding

Hiroyuki Ito, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe, and Naoki Nishida

Record of 2007 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers ( O-012 ) page： 1 2007.9

Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems

Toshiki Murata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

IEICE Technical Report SS2007-16 Vol. 107 ( 176 ) page： 1-6 2007.8

Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting

Yuji Sasada, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

IEICE Technical Report SS2007-17 Vol. 107 ( 176 ) page： 7-12 2007.8

* Transformation for Refining Unraveled Conditional Term Rewriting Systems Reviewed

Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai

Electronic Notes in Theoretical Computer Science Vol. 174 ( 10 ) page： 75-95 2007.7

Authorship：Lead author Language：English Publishing type：Research paper (scientific journal)

Unravelings, transformations from conditional term rewriting systems (CTRSs, for short) into unconditional
term rewriting systems, are valuable for analyzing properties of CTRSs. In order to completely simulate
rewrite sequences of CTRSs, the restriction by a particular context-sensitive and membership condition that
is determined by extra function symbols introduced due to the unravelings, must be imposed on the rewrite
relations of the unraveled CTRSs. In this paper, in order to weaken the context-sensitive and membership
condition, we propose a transformation applied to the unraveled CTRSs, that reduces the number of the
extra symbols. In the transformation, updating the context-sensitive condition properly, we remove the
extra symbols that satisfy a certain condition. If the transformation succeeds in removing all of the extra
symbols, we obtain the TRSs that are computationally equivalent with the original CTRSs.

Static Dependeycy Pair Method for Proving Termination of Higher-Order Rewriting Systems

Keiichirou Kusakari, Yasuo Isogai, , Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

IEICE Technical Report SS2007-12 Vol. 107 ( 99 ) page： 17-22 2007.6

Convergent Term Rewriting Systems for Inverse Computation of Injective Functions Reviewed

Naoki Nishida, Masahiko Sakai, and Terutoshi Kato

Proceedings of the 9th International Workshop on Termination (WST'07) page： 77-81 2007.6

Argument Filtering Method on Second-Order Rewriting System

Yasuo Isogai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

IEICE Technical Report SS2007-13 Vol. 107 ( 99 ) page： 23-28 2007.6

Decidability of Innermost Termination for Semi-Constructor Term Rewriting Systems

Keita Uchiyama, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

Theory of Computer Science and Its Applications, RIMS Kokyuroku (LA Symposium 2006 Winter) Vol. 1554 page： 166-170 2007.5

Confluence of Length Preserving String Rewriting Systems is Undecidable

Yi Wang, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

Theory of Computer Science and Its Applications, RIMS Kokyuroku (LA Symposium 2006 Winter) Vol. 1554 page： 171-177 2007.5

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki