Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 81 - 100 of about 247 ／ All the affair displays >>

Reversible Term Rewriting in Practice Reviewed

Naoki Nishida, Adrian Palacios, and German Vidal

Informal Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016) page： 77-85 2016.6

Language：English

A computation is considered reversible if, for each step from state S to state S', there exists a deterministic and terminating method to compute S back from S'. Reversibilization aims at producing a reversible version of an originally irreversible computation principle. Recently, we have introduced a reversible extension of term rewriting. Furthermore, we have defined an appropriate reversibilization transformation for rewrite systems so that standard rewriting becomes reversible on the transformed systems. In this paper, we focus on the potential applications of the reversibilization transformation. In particular, we show its application in the context of bidirectional program transformation and the reversibilization of cellular automata.

Extension of Separation Logic toward Verification of Functions Passed Arrays as Arguments

Shinnosuke Mizutani, Naoki Nishida, and Masahiko Sakai

the 109th Workshop on IPSJ Special Interest Group on Programming page： 1-8 2016.6

An extension of SQL for specifying combinatorial optimization problems

Yusaku Uchida, Masahiko Sakai, and Naoki Nishida

IEICE Technical Rerport Vol. 115 ( 508 ) page： 25-30 2016.3

Language：Japanese

The performance of satisfiability (SAT) solvers have incredibly improved in recent years. It is, however, difficult to design appropriate translators for solving combinatorial optimization problems by SAT-solvers. This paper proposes a description language for some combinatorial optimization problems by extending the syntax of the database query language SQL in order to enable their easy descriptions, and discusses a coding scheme of a problem specified by the language into a formula for SAT-solvers.

Program Verification Using Non-linear Loop Invariants Generated by Partially Applying an Extended Farkas' Lemma

Mawkish Yanagisawa, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 115 ( 508 ) page： 31-36 2016.3

Language：Japanese

To generate loop invariants, methods that, using Farkas' lemma, convert verification formulas obtained from a given template, a pre-condition, and a post-condtion of a program have been investigated. Farkas' lemma transforms formulas consisting of inequalities over linear polynomials into equivalent formulas. This lemma has been extended to deal with polynomials including non-linear monomials that may have function calls, and some examples that the extended Farkas' lemma succeeds in generating loop invariants having non-linear polynomials have been shown. However, it has not been discussed how useful the extended lemma is in verifying programs. In this paper, we evaluate the usefulness of a loop-invariant generation based on the extended Farkas' lemma, and propose a verification method that uses the extended lemma effectively. More precisely, using the extended lemma, we transform some of verification formulas that contain unknown coefficients for a given template, into another formula, and then we verify the validity of the formula obtained from the remaining formulas by applying an assignment for the unknown coefficients to satisfy the transformed formula.

Transforming Constrained Dependency Pairs by Narrowing

Tomohiro Sasano, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 115 ( 420 ) page： 123-128 2016.1

Language：Japanese

The dependency pair framework, a method for proving termination of term rewriting systems, has been extended for constrained term rewriting systems which are extensions of term rewriting systems by allowing rules to have guard constraints. In this paper, by removing one of the side conditions, we improve a narrowing-based transformation of constrained dependency pairs. More precisely, we show that the transformation is sound even if a dependency pair to be converted can form a self-chain such that there is no intermediate derivation.

On Proving Termination and Inductive Theorems Simultaneously for Constrained Term Rewriting Systems

Yoshifumi Kawamoto, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 115 ( 420 ) page： 75-80 2016.1

Constrained Term Rewriting tooL Reviewed

Cynthia Kop and Naoki Nishida

Proceedings of the 20th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Lecture Notes in Computer Science ( 9450 ) page： 549-557 2015.11

Language：English

This paper discusses Ctrl, a tool to analyse - both automatically and manually - term rewriting with logical constraints. Ctrl can be used with TRSs on arbitrary underlying logics, and automatically analyse various properties such as termination, confluence and quasi-reductivity. Ctrl also offers both a manual and automatic mode for equivalence tests using inductive theorem proving, giving support for and verification of "hand-written" term equivalence proofs.

DOI： 10.1007/978-3-662-48899-7_38

Maximum retaining number of learning clauses on SAT solvers for CNFs with cardinality clauses

Naohide Tsukamoto, Masahiko Sakai, Naoki Nishida, and Kenji Hashimoto

Record of 2015 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( A2-5 ) page： 1 2015.9

Reducing Relative Termination to Dependency Pair Problems Reviewed

Jose Iborra, Naoki Nishida, German Vidal, and Akihisa Yamada

Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science Vol. 9195 page： 163-178 2015.8

Authorship：Lead author Language：English

Relative termination, a generalized notion of termination, has been used in a number of different contexts like proving the confluence of rewrite systems or analyzing the termination of narrowing. In this paper, we introduce a new technique to prove relative termination by reducing it to dependency pair problems. To the best of our knowledge, this is the first significant contribution to Problem #106 of the RTA List of Open Problems. The practical significance of our method is illustrated by means of an experimental evaluation.

DOI： 10.1007/978-3-319-21401-6_11

CO3: a COnverter for proving COfluence of COnditional TRSs

Naoki Nishida, Takayuki Kuroda, Makishi Yanagisawa, and Karl Gmeiner

Proceedings of the 4th International Workshop on Confluence (IWC 2015) page： 42 2015.8

Confluence Competition 2015

Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl

Proceddings of the 25th International Conference on Automated Deduction (CADE 2015), Lecture Notes in Computer Science Vol. 9195 page： 101-104 2015.8

An Equivalent Transformation of Constrained Term Rewriting Systems by Pattern Elimination

Takahiro Nagao, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 115 ( 153 ) page： 167-172 2015.7

Language：Japanese

A constrained term rewriting system, an extension of term rewriting systems, can control application of rules by constraints such as those on integers. By partial elimination of patterns occurring in left-hand sides of rules, which preserves their meanings, one can facilitate analyzing various properties. In this article, we propose a transformation based on pattern elimination of constrained term rewriting systems that contain only patterns of interpretable terms in their left-hand sides, and show sufficient conditions for the resulting system to be equivalent to the original with respect to some properties such as sufficient completeness and innermost termination. We also propose a procedure for testing reduction completeness as an application of the transformation.

Heuristics for Automatically Proving Commutativity of Function Composition for Constrained Term Rewriting Systems

Ryutaro Kuriki, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

IEICE Technical Rerport Vol. 114 ( 510 ) page： 91-96 2015.3

A Heuristic to Solve Inverse Unfolding Problem for Functions Dealing with Tree Structure Data

Tomofumi Kato, Masanori Nagashima, Masahiko Sakai, Naoki Nishida, and Toshiki Sakabe

IEICE Technical Rerport Vol. 114 ( 510 ) page： 85-90 2015.3

A framework for computing finite SLD trees Reviewed

Naoki Nishida and German Vidal

Journal of Logical and Algebraic Methods in Programming Vol. 84 ( 2 ) page： 197-217 2015.3

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

The search space of SLD resolution, usually represented by means of a so-called SLD tree, is often infinite. However, there are many applications that must deal with possibly infinite SLD trees, like partial evaluation or some static analyses. In this context, being able to construct a finite representation of an infinite SLD tree becomes useful.

In this work, we introduce a framework to construct a finite data structure representing the (possibly infinite) SLD derivations for a goal. This data structure, called closed SLD tree, is built using four basic operations: unfolding, flattening, splitting, and subsumption. We prove some basic properties for closed SLD trees, namely that both computed answers and calls are preserved. We present a couple of simple strategies for constructing closed SLD trees with different levels of abstraction, together with some examples of its application. Finally, we illustrate the viability of our approach by introducing a test case generator based on exploring closed SLD trees.

DOI： 10.1016/j.jlamp.2014.11.006

On Efficacy of Narrowing in Proving Termination of Constrained Term Rewriting Systems

Tomoya Ueyama, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

IEICE Technical Rerport Vol. 114 ( 416 ) page： 43-48 2015.1

Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling

Koichi Ota, Takeshi Hamaguchi, Masahiko Sakai, Akihisa Yamada, Naoki Nishida, and Toshiki Sakabe

IEICE Technical Rerport Vol. 114 ( 416 ) page： 55-60 2015.1

A Finite Representation of the Narrowing Space Reviewed

Naoki Nishida and German Vidal

Revised Selected Papers of the 23rd International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science Vol. 8901 page： 54-71 2014.12

Authorship：Lead author Language：English

Narrowing basically extends rewriting by allowing free vari- ables in terms and by replacing matching with unification. As a con- sequence, the search space of narrowing becomes usually infinite, as in logic programming. In this paper, we introduce the use of some operators that allow one to always produce a finite data structure that still rep- resents all the narrowing derivations. Furthermore, we extract from this data structure a novel, compact equational representation of the (pos- sibly infinite) answers computed by narrowing for a given initial term. Both the finite data structure and the equational representation of the computed answers might be useful in a number of areas, like program comprehension, static analysis, program transformation, etc.

DOI： 10.1007/978-3-319-14125-1

Automatic Constrained Rewriting Induction towards Verifying Procedural Programs Reviewed

Cynthia Kop and Naoki Nishida

Proceedings of the 12th Asian Symposium on Programming Languages and Systems (APLAS 2014) ( 8858 ) page： 334-353 2014.11

Authorship：Lead author Language：English

This paper aims at developing a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can handle realistic functions, involving, e.g., integers and arrays. An implementation is provided.

DOI： 10.1007/978-3-319-12736-1_18

A Simple Sufficient Condition for the Completeness of a Heuristic Procedure for Inverse Unfold Problem

Masanori Nagashima, Tomofumi Kato, Masahiko Sakai, and Naoki Nishida

IPSJ Special Interest Group on Programming ( 2014-3-(9) ) page： 1-7 2014.11

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki