Faculty Profiles - NISHIDA Naoki

Papers - NISHIDA Naoki

Division display 41 - 60 of about 247 ／ All the affair displays >>

Transforming Concurrent Programs with Semaphores into Logically Constrained Term Rewrite Systems Reviewed

Misaki Kojima, Naoki Nishida, and Yutaka Matsubara

Informal Proceedings of the 7th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2020) page： 1-12 2020.6

A Case Study for Reversible Computing: Reversible Debugging of Concurrent Programs Reviewed

James Hoey, Ivan Lanese, Naoki Nishida, Irek Ulidowski, and German Vidal

Reversible Computation: Extending Horizons of Computing, Lecture Notes in Computer Science Vol. 12070 page： 108-127 2020.5

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

Reversible computing allows one to run programs not only in the usual forward direction, but also backward. A main application area for reversible computing is debugging, where one can use reversibility to go backward from a visible misbehaviour towards the bug causing it. While reversible debugging of sequential systems is well understood, reversible debugging of concurrent and distributed systems is less settled. We present here two approaches for debugging concurrent programs, one based on backtracking, which undoes actions in reverse order of execution, and one based on causal consistency, which allows one to undo any action provided that its consequences, if any, are undone beforehand. The first approach tackles an imperative language with shared memory, while the second one considers a core of the functional message-passing language Erlang. Both the approaches are based on solid formal foundations.

DOI： 10.1007/978-3-030-47361-7_5

Transforming Programs with Exclusive Control into Logically Constrained Term Rewrite Systems

Misaki Kojima, Naoki Nishida, Yutaka Matsubara, and Masahiko Sakai

IEICE Technical Rerport Vol. 119 ( 451 ) page： 31-36 2020.3

Language：Japanese

To apply Logically Constrained Term Rewrite Systems (LCTRSs, for short) to program verification, a previous work targets programs that are executed sequentially. Considering actual usage of computers, it has been expected to develop a verification method for equivalence between sequentially executed programs and their concurrent versions. In this paper, we propose a transformation of programs with exclusive control based on semaphores into LCTRSs, aiming at modeling concurrent programs by LCTRSs. To this end, we first expand arguments of a function symbol that has been introduced to represent a configuration of sequential execution, so as to store all executed processes. Next, we show how to represent operations for semaphores by rewrite rules, and show a transformation of programs with exclusive control based on semaphores into LCTRSs. We manage waiting lists for semaphores by means of number checks, avoiding recursive data structures such as lists.

Extending rewriting induction to existentially quantified equations

Kazushi Nishie, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 119 ( 246 ) page： 25-30 2019.10

Language：Japanese

In this paper, we extend rewriting induction which is developed to prove equations, to existentially quantified equations. More precisely, we first introduce existentially quantified terms into right-hand sides of rules in logically constrained term rewrite systems. Then, we formulate existentially quantified equations and extend rewriting induction for existentially quantified equations. Finally, we present an proof of inequalities by reducing them to existentially quantified equations and applying the extended rewriting induction.

CO3 (Version 2.0)

Naoki Nishida and Yuya Maeda

Proceedings of the Joint Proceedings of HOR 2019 and IWC 2019 (with system descriptions from CoCo 2019) page： 50 2019.6

Characterizing Compatible View Updates in Syntactic Bidirectionalization Reviewed

Naoki Nishida and German Vidal

Proceedings of the 11th International Conference on Reversible Computation, Lecture Notes in Computer Science Vol. 11497 page： 67-83 2019.6

Language：English

Given a function that takes a source data and returns a view, bidirectionalization aims at producing automatically a new function that takes a modified view and returns the corresponding, modified source. In this paper, we consider simple first-order functional programs specified by (conditional) term rewrite systems. Then, we present a bidirectionalization technique based on the injectivization and inversion transformations from. We also prove a number of relevant properties which ensure that changes in both the source and the view are correctly propagated and that no undesirable side-effects are introduced. Furthermore, we introduce the use of narrowing---an extension of rewriting that replaces matching with unification---to precisely characterize compatible (also called in-place) view updates so that the resulting bidirectional transformations are well defined. Finally, we discuss some directions for dealing with view updates that are not compatible.

DOI： 10.1007/978-3-030-21500-2_5

On Determinization of Inverted Grammar Programs via Context-Free Expressions Reviewed

Naoki Nishida and Minami Niwa

Informal Proceedings of the 6th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018) page： 1-15 2019.6

Authorship：Lead author Language：English

In this paper, we propose a determinization method of inverted grammar programs by means of context-free expressions which are straightforward extensions of regular expressions to context-free languages. Grammar programs are context-free grammars that an inversion method proposed by Glueck and Kawabe uses as intermediate results. We use conditional term rewriting systems (CTRSs, for short) as target programs, and our determinization method aims at transforming a given CTRS into a non-overlapping one that is semantically equivalent to the given one. To this end, we first translate a grammar program into an equivalent context-free expression. Then, by using some simple equalities of expressions, we transform the expression to a desired form. Finally, we translate the resulting expression back into an equivalent grammar program which can be translated back into a non-overlapping CTRS.

On Formalizing a Transformation of IMP Programs into Logically Constrained Term Rewriting Systems in Isabelle/HOL Reviewed

Ryota Nakayama and Naoki Nishida

Informal Proceedings of the 6th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2018) page： 1-15 2019.6

Proving Program Equivalence with Constrained Rewriting Induction and Ctrl Reviewed

Caarsten Fuhs, Cynthia Kop, and Naoki Nishida

Informal Proceedings of the 3rd Workshop on Program Equivalence and Relational Reasoning page： 1-2 2019.4

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

We prove equivalence of imperative programs by an automatic conversion of the functions in the input program to an equivalent Logically Constrained Term Rewrite System (LCTRS), followed by constrained rewriting induction (either fully automatically or guided by the user) to analyze equivalence of the corresponding functions in the LCTRS. Our approach is implemented in the tool Ctrl.

SQL queries for generating input constraints of SMT solvers from descriptions of combinatorial optimization problems

Genki Sakanashi, Masahiko Sakai, Naoki Nishida, and Kenji Hashimoto

IEICE Technical Rerport Vol. 118 ( 471 ) page： 85-90 2019.3

Language：Japanese

The authors recently proposed an SQL-based language CombSQL+ for specifying combinatorial optimization problems, and showed a solving method that uses an SMT solver. This method has an advantage that problem constraints are written in ordinary SQL queries, and hence it enables us an intuitive specification. In order to generate constraints to be solved by an SMT solver from a specification, it uses SQL queries extended for constrained tables, each of which represents a set of tables. Current extended queries, however, does not cover full-SQL query facilities, hence for this we need to develop a complex SQL-engine for constrained tables. This paper proposes a generation method of an ordinary SQL query, whose execution by an existing SQL-engine causes constraints for SMT solvers. Here, a key technique is the use of user-definable functions that may cause side-effects allowed in the database system SQLite.

On Transforming Functions Accessing Global Variables into Logically Constrained Term Rewriting Systems Reviewed

Yoshiaki Kanazawa and Naoki Nishida

Electronic Proceedings in Theoretical Computer Science Vol. 289 page： 34-52 2019.2

Language：English

In this paper, we show a new approach to transformations of an imperative program with function calls and global variables into a logically constrained term rewriting system. The resulting system represents transitions of the whole execution environment with a call stack. More precisely, we prepare a function symbol for the whole environment, which stores values for global variables and a call stack as its arguments. For a function call, we prepare rewrite rules to push the frame to the stack and to pop it after the execution. Any running frame is located at the top of the stack, and statements accessing global variables are represented by rewrite rules for the environment symbol. We show a precise transformation based on the approach and prove its correctness.

DOI： 10.4204/EPTCS.289.3

arXiv

On Transforming Narrowing Trees into Regular Tree Grammars Generating Ranges of Substitutions Reviewed

Naoki Nishida and Yuya Maeda

Electronic Proceedings in Theoretical Computer Science Vol. 289 page： 68-87 2019.2

Language：English

The grammar representation of a narrowing tree for a syntactically deterministic conditional term rewriting system and a pair of terms is a regular tree grammar that generates expressions for substitutions obtained by all possible innermost-narrowing derivations that start with the pair and end with particular non-narrowable terms. In this paper, under a certain syntactic condition, we show a transformation of the grammar representation of a narrowing tree into another regular tree grammar that overapproximately generates the ranges of ground substitutions generated by the grammar representation. In our previous work, such a transformation is restricted to the ranges w.r.t. a given single variable, and thus, the usefulness is limited. We extend the previous transformation by representing the range of a ground substitution as a tuple of terms, which is obtained by the coding for finite trees. We show a precise definition of the transformation and prove that the language of the transformed regular tree grammar is an overapproximation of the ranges of ground substitutions generated by the grammar representation. We leave an experiment to evaluate the usefulness of the transformation as future work.

DOI： 10.4204/EPTCS.289.35

arXiv

On Representation of Structures and Unions in Logically Constrained Rewriting

Yoshiaki Kanazawa, Naoki Nishida, and Masahiko Sakai

IEICE Technical Rerport Vol. 118 ( 385 ) page： 67-72 2019.1

Language：Japanese

Recently, several methods for verifying imperative programs by means of transformations into term rewriting systems have been investigated. In particular, constrained rewriting systems are popular as sources of such transformations, since logical constraints used for modeling control flows can be separated from terms that represent intermediate states of the execution of target programs.In the existing methods, data types that can be used in target programs are, however, restricted to the integers and their one-dimensional arrays, and hence we are not allowed to use other primitive data types, structures, or unions.In this article, we propose a bit-vector representation of basic data types that are recursively defined over size-fixed primitive data types, structure, and unions in the framework of logically constrained rewriting, and then propose a construction of rewrite rules that access members of structures and unions.

Extending Narrowing Trees to Basic Narrowing in Term Rewriting

Yuya Maeda, Naoki Nishida, Masahiko Sakai, and Tomoya Kobayashi

IEICE Technical Rerport Vol. 118 ( 385 ) page： 73-78 2019.1

Loop Detection by Logically Constrained Term Rewriting Reviewed

Naoki Nishida and Sarah Winkler

Proceedings of the 10th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE 2018), Lecture Notes in Computer Science Vol. 11294 page： 309-321 2018.11

Language：English

Logically constrained rewrite systems constitute a very general rewriting formalism that can capture simplification processes in various domains as well as computation in imperative programs. In both of these contexts, nontermination is a critical source of errors. We present new criteria to find loops in logically constrained rewrite systems which are implemented in the tool Ctrl. We illustrate the usefulness of these criteria in three example applications: to find loops in LLVM peephole optimizations, to detect looping program executions of C programs, and to establish nontermination of integer transition systems.

DOI： 10.1007/978-3-030-03592-1_18

A theory of reversibility for Erlang Reviewed

Ivan Lanese, Naoki Nishida, Adrian Palacios, and German Vidal

Journal of Logical and Algebraic Methods in Programming Vol. 100 page： 71-97 2018.11

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

In a reversible language, any forward computation can be undone by a finite sequence of backward steps. Reversible computing has been studied in the context of different programming languages and formalisms, where it has been used for testing and verifica- tion, among others. In this paper, we consider a subset of Erlang, a functional and concurrent programming language based on the actor model. We present a formal semantics for reversible computation in this language and prove its main properties, including its causal consistency. We also build on top of it a rollback operator that can be used to undo the actions of a process up to a given checkpoint.

DOI： 10.1016/j.jlamp.2018.06.004

On Simplification of C Programs for Asymptotic Complexity Analysis via Rewriting Analysis Tools

Kazushi Nishie, Naoki Nishida, and Masahiko Sakai

Record of 2018 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M1-5 ) page： 1 2018.9

On extention of narrowing trees to basic narrowing

Yuya Maeda, Naoki Nishida, and Masahiko Sakai

Record of 2018 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering ( M1-56 ) page： 1 2018.9

Convergence of Simultaneously and Sequentially Unraveled TRSs for Normal Conditional TRSs Reviewed

Naoki Nishida, Yuta Tsuruta, and Yoshiaki Kanazawa

Proceedings of the 7th International Workshop on Confluence (IWC 2018) page： 51-55 2018.7

Authorship：Lead author Language：English

Unravelings, which are transformations of a conditional term rewriting system (CTRS, for short) into an unconditional term rewriting system (TRS, for short), are useful to prove confluence and operational termination of some CTRSs. A simultaneous unraveling has been proposed for normal 1-CTRSs and a sequential one has been proposed for deterministic 3-CTRSs, the class of which includes normal 1-CTRSs. In this paper, we first show that for a normal 1-CTRS, the simultaneously unraveled TRS is orthogonal iff so is the sequentially unraveled one. Then, we show that for a normal 1-CTRS, if the simultaneously unraveled TRS is terminating, then so is the sequentially unraveled one. Finally, we show that for a normal 1-CTRS with termination of the unraveled TRS, the simultaneously unraveled TRS is locally confluent iff so is the sequentially unraveled one.

CO3 (Version 1.5)

Naoki Nishida, Yuta Tsuruta, and Yoshiaki Kanazawa

Proceedings of the 7th International Workshop on Confluence (IWC 2018) page： 64 2018.7

　 PREV - NEXT 　

<NISHIDA Naoki>

Papers - NISHIDA Naoki