Updated on 2024/05/20

写真a

 
NISHIDA Naoki
 
Organization
Graduate School of Informatics Department of Computing and Software Systems 1 Associate professor
Graduate School
Graduate School of Information Science
Graduate School of Informatics
Undergraduate School
School of Engineering
School of Informatics Department of Computer Science
Title
Associate professor
Contact information
メールアドレス

Degree 1

  1. Doctor of Engineering ( 2004.3   Nagoya University ) 

Research Interests 5

  1. automated theorem proving

  2. program transformation

  3. term rewriting systems

  4. functional program

  5. inverse computation

Research Areas 1

  1. Others / Others  / Fundamental Informatics

Current Research Project and SDGs 2

  1. Study on Imperative-Program Verification Using Theorem Proving Method of Constrained Rewrite Systems

  2. Research on Inversion of functional programs

Research History 4

  1. Nagoya University   Department of Computing and Software Systems, Graduate School of Informatics   Associate professor

    2017.4

      More details

    Country:Japan

    Notes:reorganization

  2. Nagoya University   Department of Information Engineering, Graduate School of Information Science   Associate professor

    2013.4 - 2017.3

      More details

    Country:Japan

  3. Nagoya University   Department of Information Engineering, Graduate School of Information Science   Assistant Professor

    2007.4 - 2013.3

      More details

    Country:Japan

    Notes:Job title changed

  4. Nagoya University   Department of Information Engineering, Graduate School of Information Science   Assistant

    2004.4 - 2007.3

      More details

    Country:Japan

Education 3

  1. Nagoya University   Graduate School of Engineering   Department of Information Engineering

    2002.4 - 2004.3

      More details

    Country: Japan

  2. Nagoya University   Graduate School of Engineering   Department of Computational Science and Engineering

    2000.4 - 2002.3

      More details

    Country: Japan

  3. Nagoya University   Faculty of Engineering   Department of Information Engineering

    1996.4 - 2000.3

      More details

    Country: Japan

Professional Memberships 3

  1. Information Processing Society of Japan

    2011.11

  2. The Institute of Electronics, Information and Communication Engineers

    2002.11

  3. Japan Society for Software Science and Technology

    2002.9

Committee Memberships 42

  1. 2023年度電子情報通信学会ソサイエティ大会   現地開催校委員  

    2022.9 - 2023.9   

  2. IFIP WG 1.6: Rewriting   Member  

    2022.8   

      More details

    Committee type:Other

  3. The 25th JSSST Workshop on Programming and Programming Languages (PPL 2014)   PC member  

    2022.8 - 2023.3   

      More details

    Committee type:Other

  4. 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)   PC member  

    2022.2 - 2022.9   

      More details

    Committee type:Other

  5. 11th International Workshop on Confluence   PC member  

    2022.1 - 2022.8   

      More details

    Committee type:Other

  6. 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)   PC member  

    2021.2 - 2021.9   

      More details

    Committee type:Other

  7. IPSJ Special Interest Group on Programming   SC member  

    2020.4 - 2024.3   

      More details

    Committee type:Academic society

  8. IPSJ Transactions on Programming Editorial Board   Editor  

    2020.4 - 2024.3   

      More details

    Committee type:Academic society

  9. 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)   PC member  

    2019.11 - 2021.7   

      More details

    Committee type:Other

  10. Confluence Competition   SC member  

    2019.9   

      More details

    Committee type:Other

  11. Information Processing Society of Japan   Representative Member  

    2019.4 - 2021.3   

      More details

    Committee type:Academic society

  12. LA Symposium 2019   Member of Secretariat  

    2019.4 - 2020.3   

      More details

    Committee type:Other

  13. 第81回情報処理学会全国大会実行委員会   プログラム編成WG委員  

    2019.1   

      More details

    Committee type:Academic society

  14. 電子情報通信学会ソフトウェアサイエンス研究専門委員会   専門委員  

    2018.6 - 2024.6   

      More details

    Committee type:Academic society

  15. IPSJ Special Interest Group on Programming   Chief examiner  

    2018.4 - 2020.3   

  16. IPSJ Transactions on Programming Editorial Board   Editor in Chief  

    2018.4 - 2020.3   

      More details

    Committee type:Academic society

  17. Information Processing Society of Japan   Member of Computer Science Area Committee  

    2018.4 - 2019.3   

      More details

    Committee type:Academic society

  18. Confluence Competition 2018 (CoCo 2018)   OC member  

    2017.10 - 2018.7   

      More details

    Committee type:Other

  19. 19th International Symposium on Principles and Practice of Declarative Programming (PPDP 2017)   PC member  

    2016.12 - 2017.10   

  20. Confluence Competition 2017 (CoCo 2017)   OC member  

    2016.10 - 2017.9   

      More details

    Committee type:Other

  21. 4th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2017)   Steering Committee, Organization Committee, and Program Committee members  

    2016.9 - 2017.9   

      More details

    Committee type:Other

  22. 8th International Symposium on Symbolic Computation in Software Science (SCSS 2017)   PC member  

    2016.8 - 2017.4   

      More details

    Committee type:Other

  23. 第79回情報処理学会全国大会実行委員会   実行委員  

    2016.8 - 2017.3   

      More details

    Committee type:Academic society

  24. 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)   PC member  

    2016.4 - 2016.9   

      More details

    Committee type:Other

  25. Confluence Competition 2016 (CoCo 2016)   OC member  

    2015.9 - 2016.9   

      More details

    Committee type:Other

  26. 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016)   Steering Committee, Organization Committee, and Program Committee members  

    2015.9 - 2016.7   

      More details

    Committee type:Other

  27. Confluence Competition 2015 (CoCo 2015)   OC member  

    2014.10 - 2015.8   

      More details

    Committee type:Other

  28. 2nd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2015)   Organization Committee co-chair and PC co-chair  

    2014.9 - 2015.7   

      More details

    Committee type:Other

  29. IPSJ Special Interest Group on Programming   SC member  

    2014.4 - 2018.3   

      More details

    Committee type:Academic society

  30. 24th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2014)   PC member  

    2014.4 - 2014.9   

  31. 3rd International Workshop on Confluence (IWC 2014)   PC member  

    2014.4 - 2014.7   

      More details

    Committee type:Other

  32. The 16th JSSST Workshop on Programming and Programming Languages (PPL 2014)   PC member  

    2014.3   

      More details

    Committee type:Other

  33. IPSJ Transactions on Programming Editorial Board   Editor  

    2013.4 - 2017.3   

      More details

    Committee type:Academic society

  34. Information Processing Society of Japan   Representative Member  

    2013.4 - 2014.4   

      More details

    Committee type:Academic society

  35. Tokai-Section Joint Conference on Electrical and Related Engineering   Member of Executive Committee  

    2012.9   

      More details

    Committee type:Academic society

  36. 23rd International Conference on Rewriting Techniques and Applications (RTA 2012)   Member of Organizing Committee  

    2012.5 - 2012.6   

      More details

    Committee type:Other

  37. 1st International Workshop on Confluence (IWC 2012)   Member of Organizing Committee  

    2012.5   

      More details

    Committee type:Other

  38. Information Processing Society of Japan Tokai Branch   Secretary  

    2012.4 - 2014.5   

      More details

    Committee type:Academic society

  39. LA Symposium 2011   Member of Secretariat  

    2011.4 - 2013.3   

      More details

    Committee type:Other

  40. 12th JSSST Workshop on Programming and Programming Languages   PC member  

    2010.3   

      More details

    Committee type:Other

  41. ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation (PEPM 2009)   PC member  

    2009.1   

      More details

    Committee type:Other

  42. MEIHOH   Secretary  

    2008.5   

      More details

    Committee type:Other

▼display all

Awards 7

  1. 情報処理学会論文編集貢献賞

    2020.5   情報処理学会  

    西田直樹

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

  2. 情報処理学会研究会活動貢献賞

    2020.2   情報処理学会  

    西田直樹

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

  3. 平成24年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞

    2013.5   電子情報通信学会ソフトウェアサイエンス研究会   Malbolge低級アセンブリプログラミングにおける制御命令の配置設計のためのSATソルバの利用

    安藤聡,酒井正彦,坂部俊樹,草刈圭一朗,西田直樹

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

  4. 平成23年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞

    2012.5   電子情報通信学会ソフトウェアサイエンス研究会   2リテラル監視法で実装されたSATソルバへの基本対称節処理機能の組み込み

    日野善信,酒井正彦,坂部俊樹,草刈圭一朗,西田直樹

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

  5. 平成23年度電子情報通信学会ソフトウェアサイエンス研究会 研究奨励賞

    2012.5   電子情報通信学会ソフトウェアサイエンス研究会   語問題を基底等式集合の語問題に帰着可能な等式集合のクラスについて

    坂井利光,酒井正彦,坂部俊樹,西田直樹,草刈圭一朗

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

  6. The Best Paper Award from IEICE

    2011.5   IEICE  

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

  7. 2002 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers

    2003.1   Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers  

     More details

    Award type:Award from Japanese society, conference, symposium, etc.  Country:Japan

▼display all

 

Papers 236

  1. A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-path Reachability Problems with Constant Destinations Reviewed International journal

    Misaki Kojima and Naoki Nishida

    Journal of Information Processing   Vol. 32   page: 417 - 435   2024.5

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (scientific journal)   Publisher:Information Processing Society of Japan  

    An all-path reachability (APR, for short) problem of a logically constrained term rewrite system (LCTRS, for short) is a pair of constrained terms representing state sets. An APR problem is demonically valid if every finite execution path from any state in the first set to an irreducible state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by an LCTRS to an APR problem with irreducible constant destinations. In this paper, by focusing on quasi-termination of constrained narrowing, we characterize a class of LCTRSs of which APR problems with constant destinations are decidable. Quasi-termination of a (constrained) term w.r.t. narrowing is the finiteness of the set of reachable narrowed (constrained) terms from the initial (constrained) term up to variable renaming (and equivalence of constraints). To this end, we first introduce an inference rule for disproofs to a proof system for APR problems with constant destinations and formulate (dis)proof trees of APR problems in the style of cyclic proofs. Secondly, to prove correctness of disproof trees, we adapt constrained narrowing to LCTRSs and show soundness of constrained narrowing of LCTRSs w.r.t. constrained rewriting. Thirdly, we show a sufficient condition of LCTRSs for quasi-termination of constrained narrowing starting from linear constrained terms that have no nesting of defined symbols: Rewrite rules are right-linear and nesting-free w.r.t. defined symbols, and the application of rewrite rules for (mutually) recursive defined symbols does not increase the height of resulting constrained terms of narrowing. Finally, we show that if a constrained term is quasi-terminating w.r.t. narrowing of an LCTRS over a sort-wise finite signature with a decidable theory, then the APR problem consisting of the constrained term and an irreducible constant is decidable.

    DOI: 10.2197/ipsjjip.32.417

  2. Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting Reviewed International journal

    Misaki Kojima and Naoki Nishida

    Journal of Logical and Algebraic Methods in Programming   Vol. 135   page: 1 - 19   2023.10

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (scientific journal)  

    A concurrent program with semaphore-based exclusive control can be modeled by a logically constrained term rewrite system. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem of the system is a pair of state sets and is demonically valid if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, we propose a weakened but easily-implementable variant of an existing proof system for all-path reachability problems. As a case study, we deal with the race freedom of concurrent programs with semaphore-based exclusive control.

    DOI: 10.1016/j.jlamp.2023.100903

  3. On Singleton Self-Loop Removal for Termination of LCTRSs with Bit-Vector Arithmetic Reviewed

    Ayuka Mastumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin

    Proceedings of the 19th International Workshop on Termination     page: 1 - 6   2023.8

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (conference, symposium, etc.)  

    As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case.

    DOI: 10.48550/arXiv.2307.14094

  4. CO3 (Version 2.4)

    Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

    Proceedings of the 12th International Workshop on Confluence     page: 67   2023.8

     More details

    Authorship:Lead author, Corresponding author   Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  5. A New Format for Rewrite Systems Reviewed International coauthorship

    Takahito Aoto, Nao Hirokawa, Dohan Kim, Misaki Kojima, Aart Middeldorp, Fabian Mitterwallner, Naoki Nishida, Teppei Saito, Jonas Schöpf, Kiraku Shintani, Rene Thiemann, and Akihisa Yamada

    Proceedings of the 12th International Workshop on Confluence     page: 32 - 37   2023.8

     More details

    Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  6. On Representations of Waiting Queues for Semaphores in Logically Constrained Term Rewrite Systems Reviewed

    Misaki Kojima and Naoki Nishida

    Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023)     page: 1 - 6   2023.7

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    A transformation of concurrent programs with semaphore-based exclusive control and waiting queues into logically constrained term rewrite systems (LCTRSs, for short) has been proposed. To represent waiting queues, the transformation adopts a turn waiting system with number tickets, while the use of usual lists is a straightforward approach. In this abstract, we show a list-based approach to waiting queues and compare the two approaches by means of verification of race freedom of a simple reader-writer example.

  7. A Nesting-Preserving Transformation of SIMP Programs into Logically Constrained Term Rewrite Systems Reviewed

    Naoki Nishida, Misaki Kojima, and Ayuka Matsumi

    Informal Proceedings of the 10th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2023)     page: 1 - 11   2023.7

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must be often useful in analyzing the transformed LCTRS, but, to use such features, we have to know how to transform the program into the LCTRS, e.g., we keep the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C integer program) into an LCTRS. The transformation is almost based on previous work and introduces the nesting of function symbols that correspond to statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness of the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

  8. On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic

    Ayuka Matsumi, Naoki Nishida, Misaki Kojima, and Donghoon Shin

    IEICE Technical Rerport   Vol. 122 ( 432 ) page: 85 - 90   2023.3

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

    Logically constrained term rewrite systems with the bit-vector theory (BV-LCTRSs, for short) are useful as models of programs written in C or other languages. During a process of Rewriting Induction for equivalence verification, we need to frequently prove termination of rewrite systems obtained by adding rewriting rules for induction hypotheses into a given rewrite system. As for term rewrite systems, the dependency pair (DP, for short) framework is used for proving termination of LCTRSs, and several kinds of DP processors are used in the framework. However, the polynomial interpretation processor, one of the most powerful processors in proving termination of LCTRSs with the integer theory, is not applicable to BV-LCTRSs. In this article, we aim at enhancing the power of proving termination of BV-LCTRSs. To this end, we propose the polynomial interpretation processor over bit-vectors and the single self-looping elimination processor as new DP processors for BV-LCTRSs.

  9. From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting Reviewed International journal

    Misaki Kojima and Naoki Nishida

    Proceedings of the 25th International Symposium on Practical Aspects of Declarative Languages, Lecture Notes in Computer Science   Vol. 13880   page: 161 - 179   2023.1

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:Springer, Cham  

    An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this paper, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.

    DOI: 10.1007/978-3-031-24841-2_11

  10. CO3 (Version 2.3)

    Naoki Nishida and Misaki Kojima

    Proceedings of the 11th International Workshop on Confluence     page: 63   2022.8

     More details

    Authorship:Lead author, Corresponding author   Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  11. Confluence Competition 2022 International coauthorship

    Raul Gutierrez, Aart Middeldorp, Naoki Nishida, and Kiraku Shintani

    Proceedings of the 11th International Workshop on Confluence     page: 54   2022.8

     More details

    Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  12. On Transforming Imperative Programs into Logically Constrained Term Rewrite Systems via Injective Functions from Configurations to Terms Reviewed

    Naoki Nishida, Misaki Kojima, and Takumi Kato

    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022)     page: 1 - 16   2022.7

     More details

    Authorship:Lead author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work converts a statement list to rewrite rules in a stepwise manner, and proves the correctness along such a conversion and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language comprises of inference rules that define transition steps of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for plain definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work, we show an injective function from configurations to terms, and reformulate the transformation by means of the injective function. The injective function maps a transition step to a reduction step, and results in a plain correctness proof.

  13. On Reducing Non-Occurrence of Specified Runtime Errors to All-Path Reachability Problems of Constrained Rewriting Reviewed

    Misaki Kojima and Naoki Nishida

    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022)     page: 1 - 16   2022.7

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    A concurrent program with semaphore-based exclusive control can be transformed into a logically constrained term rewrite system that is computationally equivalent to the program. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem is a pair of state sets and is true if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, as a case study, we show how to apply the framework to the race-freeness of semaphore-based exclusive control in the program. Finally, we show a simplified variant of a proof system for all-path reachability problems.

  14. On Transforming Rewriting-Induction Proofs for Logical-Connective-Free Sequents into Cyclic Proofs Reviewed

    Shujun Zhang and Naoki Nishida

    Informal Proceedings of the 9th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2022)     page: 1 - 14   2022.7

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    A GSC-terminating and orthogonal inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. Under certain assumptions, it has been shown that a quantifier- and cut-free cyclic proof of a sequent can be transformed into a rewriting-induction (RI, for short) proof of the corresponding term equation. The RI proof can be transformed back into the cyclic proof, but it is not known how to transform arbitrary RI proofs into cyclic proofs. In this paper, we show that for a quantifier- and logical-connective-free sequent, if there exists an RI proof of the corresponding term equation, then there exists a cyclic proof of some sequent w.r.t. some IDS such that the cyclic proof ensures the validity of the initial sequent. To this end, we show a transformation of the RI proof into such a cyclic proof, a sequent, and an IDS.

  15. Transforming orthogonal inductive definition sets into confluent term rewrite systems Reviewed International journal

    Shujun Zhang and Naoki Nishida

    Journal of Logical and Algebraic Methods in Programming   Vol. 127   page: 1 - 17   2022.6

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (scientific journal)  

    In this paper, we transform an orthogonal inductive definition set, which is a set of productions for inductive predicates, into a confluent term rewrite system such that a quantifier-free sequent is valid w.r.t. the inductive definition set if and only if an equation representing the sequent is an inductive theorem of the term rewrite system. To this end, we first propose a transformation of an orthogonal inductive definition set into a confluent term rewrite system that is equivalent to the inductive definition set in the sense of evaluating ground formulas. Then, we show that termination of the inductive definition set is proved by the generalized subterm criterion if and only if termination of the transformed term rewrite system is so. Finally, we show that the transformed term rewrite system with some rewrite rules for sequents has the expected property. In addition, we show a termination criterion for the union of term rewrite systems whose termination is proved by the generalized subterm criterion.

    DOI: 10.1016/j.jlamp.2022.100779

  16. On Transforming Cut- and Quantifier-Free Cyclic Proofs into Rewriting-Induction Proofs Reviewed International journal

    Shujun Zhang and Naoki Nishida

    Proceedings of the 16th International Symposium on Functional and Logic Programming (FLOPS 2022), Lecture Notes in Computer Science   Vol. 13215   page: 262 - 281   2022.5

     More details

    Authorship:Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)   Publisher:Springer  

    An inductive definition set (IDS, for short) of first-order predicate logic can be transformed into a many-sorted term rewrite system (TRS, for short) such that a quantifier-free sequent is valid w.r.t. the IDS if and only if a term equation representing the sequent is an inductive theorem of the TRS. In this paper, to compare rewriting induction (RI, for short) with cyclic proof systems, under certain assumptions, we show that if a sequent has a cut- and quantifier-free cyclic proof, then there exists an RI proof for a term equation of the sequent. To this end, we propose a transformation of a cut- and quantifier-free cyclic proof of the sequent into an RI proof for the corresponding equation.

    DOI: 10.1007/978-3-030-99461-7_15

  17. Implementing Determinization of Term Rewrite Systems via Equivalence of Context-Free Expressions Toward Program Inversion

    Himika Kumagai and Naoki Nishida

    Record of the 84th National Convention of IPSJ     page: 271 - 272   2022.3

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

  18. On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR

    Takumi Kato, Naoki Nishida, and Masahiko Sakai

    IEICE Technical Rerport   Vol. 121 ( 318 ) page: 89 - 94   2022.1

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

    A method to verify programs written in a simple C-like language via logically constrained term rewrite systems (LCTRS, for short) has been investigated. The method transforms a program into an LCTRS, and reduces properties of the program to those of the transformed LCTRS. In this article, we propose a transformation of LLVM IRs into LCTRSs, aiming at expanding the scope of the method. In the semantics of LLVM IRs, a configuration includes a memory and an assignment as mappings in general. On the other hand, LCTRSs used in the existing work do not deal with such mappings as built-in data, and thus, function symbols keep ranges of memories and assignments as arguments, making the transformation and its correctness proof more complicated. For this reason, we employ LCTRSs that deal with memories and assignments as built-in data, as LLVM IRs do. This makes a correctness proof of our transformation clear. More precisely, we define an injective mapping from configurations to terms. Using the mapping, we propose a transformation that generates a rewrite rule for each instruction in an LLVM IR by instantiating each inference rule of the LLVM-IR semantics which is applicable to the instruction.

  19. Lemma Generation by Lagrange Interpolation in Con- strained Rewriting Induction

    Shinya Higa, Naoki Nishida, and Masahiko Sakai

    Proceedings of the 38th Conference of Japan Society for Software Science and Technology     page: 1 - 13   2021.9

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

  20. Determinization of inverted grammar programs via context-free expressions Reviewed International journal

    Naoki Nishida and Minami Niwa

    Journal of Logical and Algebraic Methods in Programming   Vol. 122   page: 1 - 26   2021.8

     More details

    Authorship:Lead author, Corresponding author   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.2021.100688

    Other Link: http://hdl.handle.net/2237/0002001914

  21. Confluence Competition 2021 International coauthorship

    Aart Middeldorp, Naoki Nishida, Kiraku Shintani, and Johannes Waldmann

    Proceedings of the 10th International Workshop on Confluence     page: 51   2021.7

     More details

    Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  22. CO3 (Version 2.2)

    Naoki Nishida

    Proceedings of the 10th International Workshop on Confluence     page: 61   2021.7

     More details

    Authorship:Lead author, Corresponding author   Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  23. On Transforming Inductive Definition Sets into Term Rewrite Systems Reviewed

    Shujun Zhang and Naoki Nishida

    Informal Proceedings of the 8th International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2021)     page: 1 - 10   2021.7

     More details

    Authorship:Last author, Corresponding author   Language:English   Publishing type:Research paper (international conference proceedings)  

    In this paper, we transform an inductive definition set—a set of productions for inductive predicates—into a term rewrite system (TRS, for short) such that a quantifier-free sequent over the first-order logic with the inductive definition set is valid if and only if its corresponding equation is an inductive theorem of the TRS. The resulting TRS is composed of three parts: Rewrite rules for logical connectives and a binary symbol for sequents; rewrite rules for productions; rewrite rules for the co-patterns of the second part. For correctness of the resulting TRS, we assume a certain property of the inductive definition set, which is a sufficient condition for ground termination and ground confluence of the resulting TRS. The transformation aims at comparing cyclic proof systems and rewriting induction.

  24. Transforming Programs with Counting Semaphores into Logically Constrained Term Rewrite Systems

    Misaki Kojima, Naoki Nishida, and Masahiko Sakai

    Record of the 83rd National Convention of IPSJ     page: 229 - 230   2021.3

     More details

    Authorship:Corresponding author   Language:Japanese   Publishing type:Research paper (conference, symposium, etc.)  

  25. Speeding up combinatorial optimization solver CombSQL+ by introducing Pseudo-Boolean constraints

    Junichiro Kishi, Masahiko Sakai, Naoki Nishida, and Kenji Hashimoto

    IEICE Technical Rerport   Vol. 120 ( 343 ) page: 66-71   2021.1

     More details

    Language:Japanese  

    The authors have proposed a solver CombSQL+ for combinatorial optimization problems (COPs) described in extended SQL language. The system generates QFLIA constraints by executing an SQL query transformed from an input description, and then solves them by an SMT solver. This report proposes an improvement of the system to generate constraints in pseudo-Boolean forms if possible. We report that the enhancement accelerates more than seven times faster for a problem.

  26. Reversible CSP Computations Reviewed

    Carlos Galindo, Naoki Nishida, Josep Silva, and Salvador Tamarit

    IEEE Transactions on Parallel and Distributed Systems   Vol. 32 ( 6 ) page: 1425-1436   2021.1

     More details

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

    Reversibility enables a program to be executed both forwards and backwards. This ability allows programmers to backtrack the execution to a previous state. This is essential if the computation is not deterministic because re-running the program forwards may not lead to that state of interest. Reversibility of sequential programs has been well studied and a strong theoretical basis exists. Contrarily, reversibility of concurrent programs is still very young, especially in the practical side. For instance, in the particular case of the Communicating Sequential Processes (CSP) language, reversibility is practically missing. In this article, we present a new technique, including its formal definition and its implementation, to reverse CSP computations. Most of the ideas presented can be directly applied to other concurrent specification languages such as Promela or CCS, but we center the discussion and the implementation on CSP. The technique proposes different forms of reversibility, including strict reversibility and causal-consistent reversibility. On the practical side, we provide an implementation of a system to reverse CSP computations that is able to highlight the source code that is being executed in each forwards/backwards computation step, and that has been optimized to be scalable to real systems.

    DOI: 10.1109/TPDS.2021.3051747

  27. ReverCSP: Time-Travelling in CSP Computations Reviewed

    Carlos Galindo, Naoki Nishida, Josep Silva, and Salvador Tamarit

    Proceedings of the 12th International Conference on Reversible Computation, Lecture Notes in Computer Science   Vol. 12227   page: 239-245   2020.7

     More details

    Language:English  

    This paper presents reverCSP, a tool to animate both forward and backward CSP computations. This ability to reverse computations can be done step by step or backtracking to a given desired state of interest. reverCSP allows us to reverse computations exactly in the same order in which they happened, or also in a causally-consistent way. Therefore, reverCSP is a tool that can be especially useful to comprehend, analyze, and debug computations. reverCSP is an open-source project publicly available for the community. We describe the tool and its functionality, and we provide implementation details so that it can be reimplemented for other languages.

    DOI: 10.1007/978-3-030-52482-1_14

  28. Confluence Competition 2020 International coauthorship

    Aart Middeldorp, Naoki Nishida, Kiraku Shintani, and Johannes Waldmann

    Proceedings of the 9th International Workshop on Confluence     page: 53   2020.6

     More details

    Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  29. CO3 (Version 2.1)

    Naoki Nishida

    Proceedings of the 9th International Workshop on Confluence     page: 67   2020.6

     More details

    Authorship:Lead author, Corresponding author   Language:English   Publishing type:Research paper (conference, symposium, etc.)  

  30. 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

     More details

    Language:English   Publishing type:Research paper (international conference proceedings)  

  31. 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

     More details

    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

  32. 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

     More details

    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.

  33. 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

     More details

    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.

  34. 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

     More details

    Authorship:Lead author   Language:English  

  35. 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

     More details

    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

  36. 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

     More details

    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.

  37. 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

     More details

    Language:English  

    In this paper, we aim at formalizing a transformation of an IMP program into a logically constrained term rewriting system (LCTRS, for short) in Isabelle/HOL. To this end, we formalize LCTRSs and the transformation in Isabelle/HOL.

  38. 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

     More details

    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.

  39. 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

     More details

    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.

  40. 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

     More details

    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

  41. 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

     More details

    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

  42. 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

     More details

    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.

  43. 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

     More details

    Language:Japanese  

  44. 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

     More details

    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

  45. 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

     More details

    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

  46. 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

     More details

    Language:Japanese  

  47. 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

     More details

    Language:Japanese  

  48. 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

     More details

    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.

  49. 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

     More details

    Authorship:Lead author   Language:English  

  50. Narrowing Trees for Syntactically Deterministic Conditional Term Rewriting Systems Reviewed

    Naoki Nishida and Yuya Maeda

    Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs   Vol. 108   page: 26:1-26:20   2018.6

     More details

    Authorship:Lead author   Language:English  

    A narrowing tree for a constructor term rewriting system and a pair of terms is a finite representation for the space of all possible innermost-narrowing derivations that start with the pair and end with non-narrowable terms. Narrowing trees have grammar representations that can be considered regular tree grammars. Innermost narrowing is a counterpart of constructor-based rewriting, and thus, narrowing trees can be used in analyzing constructor-based rewriting to normal forms. In this paper, using grammar representations, we extend narrowing trees to syntactically deterministic conditional term rewriting systems that are constructor systems. We show that narrowing trees are useful to prove two properties of a normal conditional term rewriting system: one is infeasibility of conditional critical pairs and the other is quasi-reducibility.

    DOI: 10.4230/LIPIcs.FSCD.2018.26

  51. Confluence Competition 2018

    Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl

    Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD 2018), LIPIcs   Vol. 108   page: 32:1-32:5   2018.6

     More details

    Authorship:Lead author   Language:English  

    We report on the 2018 edition of the Confluence Competition, a competition of software tools that aim to (dis)prove confluence and related properties of rewrite systems automatically.

    DOI: 10.4230/LIPIcs.FSCD.2018.32

  52. CauDEr: A Causal-Consistent Reversible Debugger for Erlang Reviewed

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

    Proceedings of the 14th International Conference on Functional and Logic Programming, Lecture Notes in Computer Scienc   Vol. 10818   page: 247-263   2018.4

     More details

    Language:English  

    Programming languages based on the actor model, such as Erlang, avoid some concurrency bugs by design. However, other concurrency bugs, such as message order violations and livelocks, can still show up in programs. These hard-to-find bugs can be more easily detected by using causal-consistent reversible debugging, a debugging technique that allows one to traverse a computation both forward and backward. Most notably, causal consistency implies that, when going backward, an action can only be undone provided that its consequences, if any, have been undone beforehand. To the best of our knowledge, we present the first causal-consistent reversible debugger for Erlang, which may help programmers to detect and fix various kinds of bugs, including message order violations and livelocks.

    DOI: 10.1007/978-3-319-90686-7_16

  53. Rewriting induction for constrained inequalities Reviewed

    Takahiro Nagao and Naoki Nishida

    Science of Computer Programming   Vol. 155   page: 76-102   2018.4

     More details

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

    Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Direct handling of inequalities enables us to utilize transitivity of binary predicates via application of induction hypotheses. Our framework succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations. For the sake of automated reasoning, we provide a strategy for applying inference rules and evaluate its performance by means of an implementation.

    DOI: 10.1016/j.scico.2017.10.012

  54. Transforming Proof Tableaux of Hoare Logic into Inference Sequences of Rewriting Induction Reviewed

    Shinnosuke Mizutani and Naoki Nishida

    Electronic Proceedings in Theoretical Computer Science   Vol. 265   page: 35-51   2018.2

     More details

    Language:English  

    A proof tableau of Hoare logic is an annotated program with pre- and post-conditions, which corresponds to an inference tree of Hoare logic. In this paper, we show that a proof tableau for partial correctness can be transformed into an inference sequence of rewriting induction for constrained rewriting. We also show that the resulting sequence is a valid proof for an inductive theorem corresponding to the Hoare triple if the constrained rewriting system obtained from the program is terminating. Such a valid proof with termination of the constrained rewriting system implies total correctness of the program w.r.t. the Hoare triple. The transformation enables us to apply techniques for proving termination of constrained rewriting to proving total correctness of programs together with proof tableaux for partial correctness.

    DOI: 10.4204/EPTCS.265.4

  55. Transforming Dependency Chains of Constrained TRSs into Bounded Monotone Sequences of Integers Reviewed

    Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama

    Electronic Proceedings in Theoretical Computer Science   Vol. 265   page: 83-97   2018.2

     More details

    Language:English  

    In the dependency pair framework for proving termination of rewriting systems, polynomial interpretations are used to transform dependency chains into bounded decreasing sequences of integers, and they play an important role for the success of proving termination, especially for constrained rewriting systems. In this paper, we show sufficient conditions of linear polynomial interpretations for transforming dependency chains into bounded monotone (i.e., decreasing or increasing) sequences of integers. Such polynomial interpretations transform rewrite sequences of the original system into decreasing or increasing sequences independently of the transformation of dependency chains. When we transform rewrite sequences into increasing sequences, polynomial interpretations have non-positive coefficients for reducible positions of marked function symbols. We propose four DP processors parameterized by transforming dependency chains and rewrite sequences into either decreasing or increasing sequences of integers, respectively. We show that such polynomial interpretations make us succeed in proving termination of the McCarthy 91 function over the integers.

    DOI: 10.4204/EPTCS.265.7

  56. Reversible computation in term rewriting Reviewed

    Naoki Nishida, Adrian Palacios, and German Vidal

    Journal of Logical and Algebraic Methods in Programming   Vol. 94   page: 128-149   2018.1

     More details

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

    Essentially, in a reversible programming language, for each forward computation from state S to state S', there exists a constructive method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few.

    In this work, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 -> t2, we do not always have a decidable method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define two transformations, injectivization and inversion, to make a rewrite system reversible using standard term rewriting. We illustrate the usefulness of our transformations in the context of bidirectional program transformation.

    DOI: 10.1016/j.jlamp.2017.10.003

  57. CO3 (Version 1.4)

    Naoki Nishida, Yoshiaki Kanazawa,, and Karl Gmeiner

    Proceedings of the 5th International Workshop on Confluence (IWC 2016)     page: 73   2017.9

     More details

    Authorship:Lead author   Language:English  

  58. A Reversible Semantics for Erlang Reviewed

    Naoki Nishida, Adrian Palacios, and German Vidal

    Revised Selected Papers of the 26th International Conference on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science (LOPSTR 2016)   Vol. 10184   page: 259-274   2017.7

     More details

    Authorship:Lead author   Language:English  

    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 debugging and for enforcing fault-tolerance, among others. In this paper, we consider a subset of Erlang, a concurrent language based on the actor model, and formally introduce a semantics for reversible computation. To the best of our knowledge, this is the first attempt to define a reversible semantics for Erlang.

    DOI: 10.1007/978-3-319-63139-4_15

  59. A compiler that translates to Malbolge from a C-language subset containing recursive calls

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

    IEICE Technical Rerport   Vol. 117 ( 136 ) page: 145-150   2017.7

     More details

    Language:Japanese  

    Malbolge is an esoteric programming language, which is promising to protect intellectual property rights due to its difficulty of analysis. It is, however, very difficult to program because of its peculiar instructions. Tackling this problem, pseudo-instruction sequences was developed as an intermediate language for generating Malbolge programs. Nevertheless it is still difficult to program compared with ordinary languages like C. In this article, we present how to implement a compiler that translates to Malbolge from a C-language subset containing the integer type, the Boolean type, basic control structures such as while statement, and recursive calls. In the implementation, we firstly added array syntax and function syntax to pseudo-instruction sequences, and strengthen existing tools for the extention to conform with it. We next propose a translation method from C-language subset to pseudo-instruction sequences.

  60. Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Integers

    Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, and Tomoya Ueyama

    IEICE Technical Rerport   Vol. 117 ( 136 ) page: 139-144   2017.7

     More details

    Language:Japanese  

    In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations that transform dependency chains representing sequences of relevant function calls into bounded decreasing sequences of integers play an important role for the success of proving termination. In this article, we propose polynomial interpretations that transform dependency chains into bounded decreasing sequences but transform rewrite sequences of the original system into increasing sequences.We also propose polynomial interpretations that transform dependency chains into bounded increasing sequences of integers.
    We report empirical comparison results between the proposed polynomial interpretations.

  61. Verifying Procedural Programs via Constrained Rewriting Induction Reviewed

    Carsten Fuhs, Cynthia Kop, and Naoki Nishida

    ACM Transactions on Computational Logic   Vol. 18 ( 2 ) page: 14:1-14:50   2017.6

     More details

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

    This article aims to develop a verification method for procedural programs via a transformation into logically constrained term rewriting systems (LCTRSs). To this end, we extend transformation methods based on integer term rewriting systems to handle arbitrary data types, global variables, function calls, and arrays, and to encode safety checks. Then we adapt existing rewriting induction methods to LCTRSs and propose a simple yet effective method to generalize equations. We show that we can automatically verify memory safety and prove correctness of realistic functions. Our approach proves equivalence between two implementations; thus, in contrast to other works, we do not require an explicit specification in a separate specification language.

    DOI: 10.1145/3060143

  62. Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness

    Takayuki Kuroda, Naoki Nishida, and Hiroyuki Seki

    IEICE Technical Rerport   Vol. 116 ( 512 ) page: 103-108   2017.3

     More details

    Language:Japanese  

    A transformational approach to confluence proofs for conditional term rewriting systems (CTRS) has been investigated, but confluence of a CTRS defining sorting over natural numbers has not been proved yet by any existing confluence prover. Such a CTRS defines behavior of function symbols hierarchically, called a hierarchical CTRS, and is not sufficiently complete. In this article, we propose a method to prove confluence of hierarchical CTRSs that are not sufficiently complete. More precisely, we first extend rewriting induction for conditional equations to TRSs that are not sufficiently complete, and then we prove joinability of a conditional critical pair by inducing other conditions from the original conditional part. Next, we design a simplification order that takes conditional parts of rewrite rules into account, and propose a method to prove termination of hierarchical CTRSs by means of the designed simplification order.

  63. Relative Termination via Dependency Pairs Reviewed

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

    Journal of Automated Reasoning   Vol. 58 ( 3 ) page: 391-411   2017.3

     More details

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

    A term rewrite system is terminating when no infinite reduction sequences are possible. Relative termination generalizes termination by permitting infinite reductions as long as some distinguished rules are not applied infinitely many times. Relative termination is thus a fundamental notion that has been used in a number of different contexts, like analyzing the confluence of rewrite systems or the termination of narrowing. In this work, we introduce a novel 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. We first present a general approach that is then instantiated to provide a concrete technique for proving relative termination. The practical significance of our method is illustrated by means of an experimental evaluation.

    DOI: 10.1007/s10817-016-9373-5

  64. Sound Structure-Preserving Transformation for Ultra-Weakly-Left-Linear Deterministic Conditional Term Rewriting Systems Reviewed

    Ryota Nakayama, Naoki Nishida, and Masahiko Sakai

    Proceedings of the 3rd International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Electronic Proceedings in Theoretical Computer Science   Vol. 235   page: 62-77   2017.1

     More details

    Language:English  

    In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is a sound structure-preserving transformation for weakly-left-linear deterministic conditional term rewriting systems. More precisely, we show that every weakly-left-linear deterministic conditional term rewriting system can be converted to an equivalent weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting system and prove that the SR transformation is sound for weakly-left-linear and ultra-weakly-left-linear deterministic conditional term rewriting systems. Here, soundness for a conditional term rewriting system means that reduction of the transformed unconditional term rewriting system creates no undesired reduction sequence for the conditional system.

    DOI: 10.4204/EPTCS.235.5

    arXiv

  65. Notes on Confluence of Ultra-WLL SDCTRSs via a Structure-Preserving Transformation Reviewed

    Naoki Nishida

    Proceedings of the 5th International Workshop on Confluence (IWC 2016)     page: 60-64   2016.9

     More details

    Authorship:Lead author   Language:English  

    A structure-preserving transformation proposed by Serbanuta and Rosu for strongly or syntactically deterministic conditional term rewriting systems (SDCTRSs) that are ultra-left-linear has been shown to be applicable to weakly-left-linear (WLL) and ultra-WLL SDCTRSs without any change, and sound for such DCTRSs even if they are not SDCTRSs. In this paper, we show a confluent, WLL, and ultra-WLL DCTRS that is not an SDCTRS such that the transformed TRS is not confluent. We also show that for a WLL and ultra-WLL SDCTRS, if the transformed TRS is confluent, then so is the SDCTRS.

  66. CO3 (Version 1.3)

    Naoki Nishida, Takayuki Kuroda, and Karl Gmeiner

    Proceedings of the 5th International Workshop on Confluence (IWC 2016)     page: 74   2016.9

     More details

    Authorship:Lead author   Language:English  

  67. Proving inductive validity of constrained inequalities Reviewed

    Takahiro Nagao and Naoki Nishida

    Proceedings of the 18th International Symposium on Principles and Practice of Declarative Programming (PPDP 2016)     page: 50-61   2016.9

     More details

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

    Rewriting induction (RI) frameworks consist of inference rules to prove equations to be inductive theorems of a given term rewriting system, i.e., to be inductively valid w.r.t. reduction of the given system. To prove inductive validity of inequalities within such frameworks, one may reduce inequalities to equations. However, it is often hard to prove inductive validity of such reduced equations within the existing RI frameworks due to their indirect handling of inequalities. In this paper, we adapt the notion of inductive theorems to inequalities and propose an RI framework for directly proving inductive validity of inequalities of constrained term rewriting systems. Within the framework, we handle inequalities that may contain function symbols defined in a given rewriting system but not necessarily interpreted by the built-in semantics. Direct handling of inequalities facilitates the utilization of transitivity of magnitude relations via inequalities obtained as induction hypotheses. Our approach succeeds in proving inductive validity of some inequalities that are hard to verify within the existing RI frameworks for equations.

    DOI: 10.1145/2967973.2968598

  68. An intermediate language for a compiler generating highly obfuscated Malbolge codes

    Shohei Kobe, Masahiko Sakai, Naoki Nishida, and Hiroyuki Seki

    IEICE Technical Rerport   Vol. 116 ( 127 ) page: 105-110   2016.7

     More details

    Language:Japanese  

  69. Reversible Term Rewriting Reviewed

    Naoki Nishida, Adrian Palacios, and German Vidal

    Proceedings of the 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), LIPIcs   Vol. 52   page: 28:1-28:18   2016.6

     More details

    Language:English  

    Essentially, in a reversible programming language, for each forward computation step from state S to state S', there exists a constructive and deterministic method to go backwards from state S' to state S. Besides its theoretical interest, reversible computation is a fundamental concept which is relevant in many different areas like cellular automata, bidirectional program transformation, or quantum computing, to name a few. In this paper, we focus on term rewriting, a computation model that underlies most rule-based programming languages. In general, term rewriting is not reversible, even for injective functions; namely, given a rewrite step t1 -> t2, we do not always have a decidable and deterministic method to get t1 from t2. Here, we introduce a conservative extension of term rewriting that becomes reversible. Furthermore, we also define a transformation to make a rewrite system reversible using standard term rewriting.

    DOI: 10.4230/LIPIcs.FSCD.2016.28

  70. 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

     More details

    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.

  71. 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

     More details

    Language:Japanese  

  72. 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

     More details

    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.

  73. 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

     More details

    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.

  74. Transforming Constrained Dependency Pairs by Narrowing

    Tomohiro Sasano, Naoki Nishida, and Masahiko Sakai

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

     More details

    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.

  75. 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

     More details

    Language:Japanese  

  76. 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

     More details

    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

  77. 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

     More details

    Language:Japanese  

  78. 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

     More details

    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

  79. 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

     More details

    Authorship:Lead author   Language:English  

  80. 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

     More details

    Language:English  

    Confluence is one of the central properties of rewriting. Our competition aims to foster the development of techniques for proving/disproving confluence of various formalisms of rewriting automatically. We explain the background and setup of the 4th Confluence Competition.

    DOI: 10.1007/978-3-319-21401-6_5

  81. 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

     More details

    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.

  82. 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

     More details

    Language:Japanese  

  83. 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

     More details

    Language:Japanese  

  84. 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

     More details

    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

  85. 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

     More details

    Language:Japanese  

  86. 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

     More details

    Language:Japanese  

  87. 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

     More details

    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

  88. 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

     More details

    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

  89. 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

     More details

    Language:English  

  90. On Lemma Generation in Rewriting Induction for Constrained Term Rewriting Systems by Using Commutativity of Function Composition

    Ryutaro Kuriki, Naoki Nishida, and Masahiko Sakai

    Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering   ( M4-1 ) page: 1   2014.9

     More details

    Language:Japanese  

  91. On a Procedure for Proving Confluence of Conditional Term Rewriting Systems by Using Condition Elimination

    Makishi Yanagisawa, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering   ( M4-4 ) page: 1   2014.9

     More details

    Language:Japanese  

  92. On Reducing the Frequency of Checking Validity of Presburger Formulas in the Dependency Pair Method for Constrained Term Rewriting Systems

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

    Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering   ( M4-5 ) page: 1   2014.9

     More details

    Language:Japanese  

  93. On a Sufficient Condition for Argument Filterings to Preserve Equivalence between Functions in Term Rewriting

    Yoshifumi Kawamoto, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering   ( M4-2 ) page: 1   2014.9

     More details

    Language:Japanese  

  94. On a Necessary and Sufficient Condition for Equations to Represent Equivalence of Functions in Constrained Term Rewriting

    Takumi Kataoka, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Record of 2014 Tokai-Section Joint Conference on Electrical, Electronics, Information, and Related Engineering   ( M4-4 ) page: 1   2014.9

     More details

    Language:Japanese  

  95. On Improving Termination Preservability of Transformations from Procedural Programs into Rewrite Systems by Using Loop Invariants Reviewed

    Naoki Nishida and Takumi Kataoka

    Proceedings of the 14th International Workshop on Termination (WST 2014)     page: 1-5   2014.7

     More details

    Authorship:Lead author   Language:English  

    Recently, to analyze procedural programs by using techniques in the field of term rewriting, several transformations of a program into a rewrite system have been developed. Such transformations are basically complete in the sense of computation, and e.g., termination of the rewrite system ensures termination of the program. However, in general, termination of the program is not preserved by the transformations and, thus, the preservation of termination is a common interesting problem. In this paper, we discuss the improvement of a transformation from a simple procedural program over integers into a constrained term rewriting system by appending loop invariants to loop conditions of "while" statements so as to preserve termination as much as possible.

  96. Notes on Structure-Preserving Transformations of Conditional Term Rewrite Systems Reviewed

    Karl Gmeiner and Naoki Nishida

    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics   Vol. 40   page: 3-14   2014.7

     More details

    Language:English  

    Transforming conditional term rewrite systems (CTRSs) into unconditional systems (TRSs) is a common approach to analyze properties of CTRSs via the simpler framework of unconditional rewriting. In the past many different transformations have been introduced for this purpose. One class of transformations, so-called unravelings, have been analyzed extensively in the past. In this paper we provide an overview on another class of transformations that we call structure-preserving transformations. In these transformations the structure of the conditional rule, in particular their left-hand side is preserved in contrast to unravelings. We provide an overview of transformations of this type and define a new transformation that improves previous approaches.

    DOI: 10.4230/OASIcs.WPTE.2014.3

  97. On Proving Soundness of the Computationally Equivalent Transformation for Normal Conditional Term Rewriting Systems by Using Unravelings Reviewed

    Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics   Vol. 40   page: 39-50   2014.7

     More details

    Authorship:Lead author   Language:English  

    In this paper, we show that the SR transformation, a computationally equivalent transformation proposed by Serbanuta and Rosu, is sound for weakly left-linear normal conditional term rewriting systems (CTRS). Here, soundness for a CTRS means that reduction of the transformed unconditional term rewriting system (TRS) creates no undesired reduction for the CTRS. We first show that every reduction sequence of the transformed TRS starting with a term corresponding to the one considered on the CTRS is simulated by the reduction of the TRS obtained by the simultaneous unraveling. Then, we use the fact that the unraveling is sound for weakly left-linear normal CTRSs.

    DOI: 10.4230/OASIcs.WPTE.2014.39

  98. Inverse Unfold Problem and Its Heuristic Solving Reviewed

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

    Proceedings of the First International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2014), OpenAccess Series in Informatics   Vol. 40   page: 27-38   2014.7

     More details

    Language:English  

    Unfold/fold transformations have been widely studied in various programming paradigms and are used in program transformations, theorem proving, and so on. This paper, by using an example, show that restoring an one-step unfolding is not easy, i.e., a challenging task, since some rules used by unfolding may be lost. We formalize this problem by regarding one-step program transformation as a relation. Next we discuss some issues on a specific framework, called pure-constructor systems, which constitute a subclass of conditional term rewriting systems. We show that the inverse of T preserves rewrite relations if T preserves rewrite relations and the signature. We propose a heuristic procedure to solve the problem, and show its successful examples. We improve the procedure, and show examples for which the improvement takes effect.

    DOI: 10.4230/OASIcs.WPTE.2014.27

  99. On Proving Confluence of Conditional Term Rewriting Systems via the Computationally Equivalent Transformation Reviewed

    Naoki Nishida, Makishi Yanagisawa, and Karl Gmeiner

    Proceedings of the 3rd International Workshop on Confluence (IWC 2014)     page: 24-28   2014.7

     More details

    Authorship:Lead author   Language:English  

    This paper improves the existing criterion for proving confluence of a normal conditional term rewriting system (CTRS) via the Serbanuta-Rosu transformation, a computationally equivalent transformation of CTRSs into unconditional term rewriting systems (TRS), showing that a weakly left-linear normal CTRS is confluent if the transformed TRS is confluent. Then, we discuss usefulness of the optimization of the Serbanuta-Rosu transformation, which has informally been proposed in the literature.

  100. Inverse Unfold Problem and Its Heuristic Solving

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

    IEICE Technical Rerport   Vol. 113 ( 489 ) page: 13-18   2014.3

     More details

    Language:Japanese  

  101. On Detecting Useless Transition Rules of Constrained Tree Automata

    Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Kenji Hashimoto

    IEICE Technical Rerport   Vol. 113 ( 489 ) page: 31-36   2014.3

     More details

    Language:Japanese  

  102. Conversion to tail recursion in term rewriting Reviewed

    Naoki Nishida and German Vidal

    The Journal of Logic and Algebraic Programming   Vol. 83 ( 1 ) page: 53-63   2014.1

     More details

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

    Tail recursive functions are a special kind of recursive functions where the last action in their body is the recursive call. Tail recursion is important for a number of reasons (e.g., they are usually more efficient). In this article, we introduce an automatic transformation of first-order functions into tail recursive form. Functions are defined using a (first-order) term rewrite system. We prove the correctness of the transformation for constructor-based reduction over constructor systems (i.e., typical first-order functional programs).

    DOI: 10.1016/j.jlap.2013.07.001

  103. On Constructing Constrained Tree Automata Recognizing Ground Instances of Constrained Terms Reviewed

    Naoki Nishida, Masahiko Sakai, and Yasuhiro Nakano

    Proceedings of the 2nd International Workshop on Trends in Tree Automata and Tree Transducers (TTATT 2013), Electronic Proceedings in Theoretical Computer Science   Vol. 134   page: 1-10   2013.10

     More details

    Authorship:Lead author   Language:English  

    An inductive theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision procedure for reduction-completeness of constrained terms. In addition, the sufficient complete property of constrained term rewriting systems enables us to relax the side conditions of some inference rules in the proving method. These two properties can be reduced to intersection emptiness problems related to sets of ground instances for constrained terms. This paper proposes a method to construct deterministic, complete, and constraint-complete constrained tree automata recognizing ground instances of constrained terms.

    DOI: 10.4204/EPTCS.134.1

  104. On Reducibility of Word Problems for Equations to Those for Ground Equations

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

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M4-4 ) page: 1   2013.9

     More details

    Language:Japanese  

  105. Generation of Loop Invariants Consisting of Non-Linear Inequalities for Programs with Arrays

    Junichiro Higashino, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari and Naoki Nishida

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M4-6 ) page: 1   2013.9

     More details

    Language:Japanese  

  106. On Local Strategies for Automated Inductive-Theorem Proving on Simply Typed Term Rewriting Systems

    Hisashi Kamiya, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M4-3 ) page: 1   2013.9

     More details

    Language:Japanese  

  107. Designing Higher-order Lexicographic Path Ordering with Currying

    Honami Matsubara, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M4-5 ) page: 1   2013.9

     More details

    Language:Japanese  

  108. Development of an Interpreter Dynamically Checking Assertions on Pointers in Programs

    Yoshihiro Mokutani, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari and Naoki Nishida

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M4-7 ) page: 1   2013.9

     More details

    Language:Japanese  

  109. Use of Loop Invariants for Improving Termination Preservability of Transformations from Procedural Programs to Rewriting Systems

    Takumi Kataoka, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe and Keiichirou Kusakari

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M2-6 ) page: 1   2013.9

     More details

    Language:Japanese  

  110. Evaluation of Parallel Execution of an Implementation of Breadth-First-Search-based Completion Procedures in Erlang

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

    Record of 2013 Tokai-Section Joint Conference on Electrical and Related Engineering   ( M2-5 ) page: 1   2013.9

     More details

    Language:Japanese  

  111. Term Rewriting with Logical Constraints Reviewed

    Cynthia Kop and Naoki Nishida

    Proceedings of the 9th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence   ( 8152 ) page: 343-358   2013.9

     More details

    Authorship:Lead author   Language:English  

  112. Malbolge with 20trits word length and its programming support tool

    Tatsuki Kato, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari and Naoki Nishida

    IEICE Technical Rerport   Vol. 113 ( 159 ) page: 73-78   2013.7

     More details

    Language:Japanese  

  113. Proving Confluence of Conditional Term Rewriting Systems via Unravelings Reviewed

    Karl Gmeiner, Naoki Nishida and Bernhard Gramlich

    Proceedings of the 2nd International Workshop on Confluence     page: 35-39   2013.6

     More details

    Language:English  

  114. Computing More Specific Versions of Conditional Rewriting Systems Reviewed

    Naoki Nishida and German Vidal

    Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science   Vol. 7844   page: 137-154   2013.4

     More details

    Authorship:Lead author   Language:English  

  115. Improving Determinization of Grammar Programs for Program Inversion Reviewed

    Minami Niwa, Naoki Nishida, and Masahiko Sakai

    Revised Selected Papers of the 22nd International Symposium on Logic-Based Program Synthesis and Transformation, Lecture Notes in Computer Science   Vol. 7844   page: 155-175   2013.4

     More details

    Language:English  

  116. On Composing the Simplex Method and Gomory Cut for Deriving Integer Assignments

    Masaaki Fushimi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe

    IEICE Technical Rerport   Vol. 112 ( 458 ) page: 109-114   2013.3

     More details

    Language:Japanese  

  117. Construction of Constrained Tree Automata Recognizing Ground Instances of Constrained Terms

    Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

    IEICE Technical Rerport   Vol. 112 ( 373 ) page: 7-12   2013.1

     More details

    Language:Japanese  

  118. Using SAT Solvers for Solving Control-Instruction Layout Problems in Low-Level Assembly Programming for Malbolge

    Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari and Naoki Nishida

    IEICE Technical Rerport   Vol. 112 ( 373 ) page: 25-30   2013.1

     More details

    Language:Japanese  

  119. A SAT Encoding for Finding Operation Sequences of Malbolge that Implement Trit-wise Functions

    Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari and Naoki Nishida

    IEICE Technical Rerport   Vol. 112 ( 275 ) page: 7-12   2012.11

     More details

    Language:Japanese  

  120. Formula transformation for sequential composition of Cooper's quantifier elimination and the general simplex method

    Masaaki Fushimi, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, and Keiichirou Kusakari

    Record of 2012 Tokai-Section Joint Conference on Electrical and Related Engineering   ( A4-2 ) page: 1   2012.9

     More details

    Language:Japanese  

  121. On Constructing Constrained Tree Automaton Recognizing Ground Instances of Constrained Terms

    Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

    Record of 2012 Tokai-Section Joint Conference on Electrical and Related Engineering   ( A4-4 ) page: 1   2012.9

     More details

    Language:Japanese  

  122. Currying for Proving Termination of Simply-Typed Term Rewriting Systems

    Keisuke Kurata, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

    Record of 2012 Tokai-Section Joint Conference on Electrical and Related Engineering   ( A4-3 ) page: 1   2012.9

     More details

    Language:Japanese  

  123. Soundness of Unravelings for Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity Invited Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Logical Methods in Computer Science   Vol. 8 ( 3-4 ) page: 1-49   2012.8

     More details

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

    Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound w.r.t. reduction for every CTRS, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for a deterministic CTRS is sound w.r.t. reduction if the corresponding unraveled TRS is left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling. Finally, we show that soundness of Ohlebusch's unraveling is the weakest in soundness of the other unravelings and a transformation, proposed by Serbanuta and Rosu, for (normal) deterministic CTRSs, i.e., soundness of them respectively implies that of Ohlebusch's unraveling.

    DOI: 10.2168/LMCS-8(3:4)2012

  124. On Extending Matching Operation in Grammar Programs for Program Inversion

    Minami Niwa, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe and Keiichirou Kusakari

    IEICE Technical Rerport   Vol. 112 ( 164 ) page: 103-108   2012.7

     More details

    Language:English  

  125. Constrained Tree Automata and their Closure Properties Reviewed

    Naoki Nishida, Futoshi Nomura, Katsuhisa Kurahashi and Masahiko Sakai

    Proceedings of the 1st International Workshop on Trends in Tree Automata and Tree Transducers     page: 24-34   2012.6

     More details

    Authorship:Lead author   Language:English  

  126. More Specific Term Rewriting Systems Reviewed

    Naoki Nishida and German Vidal

    Proceedings of the 21st International Workshop on Functional and (Constraint) Logic Programming     page: 1-15   2012.5

     More details

    Authorship:Lead author   Language:English  

  127. Introducing Array Mechanism into High-Level Assembly Language for Malbolge

    Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari and Naoki Nishida

    IEICE Technical Rerport   Vol. 112 ( 23 ) page: 43-49   2012.5

     More details

    Language:Japanese  

  128. A Sound Type System for Typing Runtime Errors Reviewed

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

    IPSJ Transactions on Programming,   Vol. 5 ( 2 ) page: 16-24   2012.3

     More details

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

  129. On Rewriting Induction for Simply-typed Term Rewriting Systems

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

    IEICE Technical Rerport   Vol. 111 ( 406 ) page: 51-56   2012.1

     More details

    Language:Japanese  

  130. On class of equation sets whose word problems are reducible to those of ground equation sets

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

    IEICE Technical Rerport   Vol. 111 ( 406 ) page: 45-49   2012.1

     More details

    Language:Japanese  

  131. Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls

    Eiichi Suzuki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari and Naoki Nishida

    IEICE Technical Rerport   Vol. 111 ( 406 ) page: 39-44   2012.1

     More details

    Language:Japanese  

  132. On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems

    Kazuhiro Ooi, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe and Naoki Nishida

    IEICE Technical Rerport   Vol. 111 ( 406 ) page: 57-62   2012.1

     More details

    Language:Japanese  

  133. Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme

    Yoshizane Hino, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Rerport   Vol. 111 ( 268 ) page: 67-72   2011.10

     More details

    Language:Japanese  

  134. Verification of Equivalence between Functions in Constrained Term Rewriting Systems via Tree Homomorphisms

    Kazuya Takakuwa, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

    Proceedings of the 28th Conference of Japan Society for Software Science and Technology   ( 7B-1 ) page: 1-12   2011.9

     More details

    Language:Japanese  

  135. Disproving and Postulating for Multi-Context Rewriting Induction

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

    Proceedings of the 28th Conference of Japan Society for Software Science and Technology   ( 1A-4 ) page: 1-12   2011.9

     More details

    Language:Japanese  

  136. Introducing Addition Instruction into High-Level Assembly Language for Malbolge

    Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

    Proceedings of the 28th Conference of Japan Society for Software Science and Technology   ( 5A-3 ) page: 1-12   2011.9

     More details

    Language:Japanese  

  137. On Automatic Generation of Loop Invariants for Programs with Function Calls

    Eiichi Suzuki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari and Naoki Nishida

    Record of 2011 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( H1-5 ) page: 1   2011.9

     More details

    Language:Japanese  

  138. Decidability of Termination for Linear Left-Shallow Term Rewriting Systems

    Tatsuya Hattori, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

    Record of 2011 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( H1-6 ) page: 1   2011.9

     More details

    Language:Japanese  

  139. Decidability of Reachability for Right-shallow Context-sensitive Term Rewriting Systems Reviewed

    Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

    IPSJ Transactions on Programming,   Vol. 4 ( 4 ) page: 12-35   2011.9

     More details

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

  140. Decidability and Undecidability of Reachability for Right-Linear Left-Shallow Non-Erasing Term Rewriting Systems

    Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

    LA Symposium 2011 Summer   ( 15 ) page: 1-10   2011.7

     More details

    Language:English  

  141. On Proving Termination of Constrained Term Rewrite Systems by Eliminating Edges from Dependency Graphs Reviewed

    Tsubasa Sakata, Naoki Nishida, and Toshiki Sakabe

    Proceedings of the 20th International Workshop on Functional and (Constraint) Logic Programming, Lecture Notes in Computer Science   Vol. 6816   page: 138-155   2011.7

     More details

    Language:English  

    In this paper, we propose methods for proving termination of constrained term rewriting systems, where constraints are interpreted by built-in semantics given by users, and rewrite rules are assumed to be sound for the interpretation. To this end, we extend the dependency pair framework for proving termination of unconstrained term rewriting systems to constrained term rewriting systems. Moreover, we extend the dependency pair framework so that dependency pair processors take a subgraph of the dependency graph as input and they output a finite set of graphs which can be obtained by eliminating nodes and/or edges from the input graph.

    DOI: 10.1007/978-3-642-22531-4_9

  142. Soundness of Unravelings for Deterministic Conditional Term Rewriting Systems via Ultra-Properties Related to Linearity Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPICcs   Vol. 10   page: 267-282   2011.5

     More details

    Authorship:Lead author   Language:English  

    Unravelings are transformations from a conditional term rewriting system (CTRS, for short) over an original signature into an unconditional term rewriting systems (TRS, for short) over an extended signature. They are not sound for every CTRS w.r.t. reduction, while they are complete w.r.t. reduction. Here, soundness w.r.t. reduction means that every reduction sequence of the corresponding unraveled TRS, of which the initial and end terms are over the original signature, can be simulated by the reduction of the original CTRS. In this paper, we show that an optimized variant of Ohlebusch's unraveling for deterministic CTRSs is sound w.r.t. reduction if the corresponding unraveled TRSs are left-linear or both right-linear and non-erasing. We also show that soundness of the variant implies that of Ohlebusch's unraveling.

    DOI: 10.4230/LIPIcs.RTA.2011.267

  143. Program Inversion for Tail Recursive Functions Reviewed

    Naoki Nishida and German Vidal

    Proceedings of the 22nd International Conference on Rewriting Techniques and Applications, LIPIcs   Vol. 10   page: 283-298   2011.5

     More details

    Authorship:Lead author   Language:English  

    Program inversion is a fundamental problem that has been addressed in many different programming settings and applications. In the context of term rewriting, several methods already exist for computing the inverse of an injective function. These methods, however, usually return non-terminating inverted functions when the considered function is tail recursive. In this paper, we propose a direct and intuitive approach to the inversion of tail recursive functions. Our new technique is able to produce good results even without the use of an additional post-processing of determinization or completion. Moreover, when combined with a traditional approach to program inversion, it constitutes a promising approach to define a general method for program inversion. Our experimental results confirm that the new technique compares well with previous approaches.

    DOI: 10.4230/LIPIcs.RTA.2011.283

  144. Tree Automata with Constraints and their Closure-Properties

    Katsuhisa Kurahashi, Masahiko Sakai, Naoki Nishida, Futoshi Nomura, Toshiki Sakabe, Keiichirou Kusakari

    IEICE Technical Rerport   Vol. 110 ( 458 ) page: 61-66   2011.3

     More details

    Language:Japanese  

  145. On non-termination proof of right-linear and right-shallow term rewriting systems based on forward narrowing

    Tatsuya Hattori, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari and Toshiki Sakabe

    IEICE Technical Report SS2010-44   Vol. 110 ( 336 ) page: 31-36   2010.12

     More details

    Language:Japanese  

  146. Proposal of Abstract DPLL Algorithm Modulo Equational Theories

    Tatsuya Baba, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari, and Masahiko Sakai

    IEICE Technical Report SS2010-36   Vol. 110 ( 227 ) page: 49-54   2010.10

     More details

    Language:Japanese  

  147. On Turing Compeleteness of an Esoteric Language, Malbolge

    Satoshi Nagasaka, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2010-37   Vol. 110 ( 227 ) page: 55-60   2010.10

     More details

    Language:Japanese  

  148. SAT Solver for CNF Formulas with Elementary Symmetric Clauses based on Two Counter Scheme

    Yoshizane Hino, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe, and Naoki Nishida

    Record of 2010 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( D3-5 ) page: 1   2010.8

     More details

    Language:Japanese  

  149. Proposal of Abstract DPLL Algorithm Modulo Equational Theories

    Tatsuya Baba, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    Record of 2010 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( D3-4 ) page: 1   2010.8

     More details

    Language:Japanese  

  150. Efficient Verification of Equivalence between Functions in Constrained Term Rewriting Systems

    Kazuya Takakuwa, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

    Record of 2010 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( D3-6 ) page: 1   2010.8

     More details

    Language:Japanese  

  151. Termination of Narrowing via Termination of Rewriting Reviewed

    Naoki Nishida and Germán Vidal

    Applicable Algebra in Engineering, Communication and Computing   Vol. 21 ( 3 ) page: 177-225   2010.5

     More details

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

  152. Goal-directed and Relative Dependency Pairs for Proving the Termination of Narrowing Reviewed

    José Iborra, Naoki Nishida, and Germán Vidal

    Postproceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009), Lecture Notes in Computer Science   Vol. 6037   page: 52-66   2010.4

     More details

    Language:English  

  153. Proving Injectivity of Functions via Program Inversion in Term Rewriting Reviewed

    Naoki Nishida and Masahiko Sakai

    Proceedings of the 10th International Symposium on Functional and Logic Programming (FLOPS 2010), Lecture Notes in Computer Science   Vol. 6009   page: 288-303   2010.4

     More details

    Authorship:Lead author   Language:English  

  154. Solving Satisfiability of CNF Formulas with Clauses based on Elementary Symmetric Functions Reviewed

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

    The IEICE Transactions on Information and Systems   Vol. J93-D ( 1 ) page: 1-9   2010.1

     More details

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

  155. Program Generation Based on Transformation of Conditional Equations

    Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida, and Keiichirou Kusakari

    IEICE Technical Report SS2009-41   Vol. 109 ( 343 ) page: 37-42   2009.12

     More details

    Language:Japanese  

  156. Argument Filtering and Usable Rules in Higher-Order Rewrite Systems

    Sho Suzuki, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, and Naoki Nishida

    IEICE Technical Report SS2009-39   Vol. 109 ( 343 ) page: 25-30   2009.12

     More details

    Language:Japanese  

  157. On Decidability of Context-Sensitive Termination for Right-Linear Right-Shallow Term Rewriting Systems

    Yoshimasa Mishuku, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2009-40   Vol. 109 ( 343 ) page: 31-36   2009.12

     More details

    Language:Japanese  

  158. Improving the Termination Analysis of Narrowing in Left-Linear Constructor Systems Reviewed

    José Iborra, Naoki Nishida, and Germán Vidal

    Proceedings of the 19th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2009)     page: 9 pages   2009.9

     More details

    Language:English  

    In this extended abstract, we introduce an extension of a previous technique
    for proving the termination of narrowing. Basically, given a rewrite system
    and an argument filtering, the previous technique required the filtered
    program to be free of extra-variables. In this work, we transform the original
    rewrite system so that, in some cases (namely when the filtered rewrite system
    is left-shallow), termination can still be proved despite the occurrence of
    extra-variables in the filtered system.

  159. Lemma Generation Method in Rewriting Induction for Constrained Term Rewriting Systems

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

    Proceedings of the 26th Conference of Japan Society for Software Science and Technology (JSSST)   ( 7B-2 ) page: 1-14   2009.9

     More details

    Language:Japanese  

  160. Context-Sensitive Innermost Reachability is Decidable for Linear Right-Shallow Term Rewriting Systems Reviewed

    Yoshiharu Kojima, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

    IPSJ Transactions on Programming,   Vol. 2 ( 3 ) page: 20-32   2009.7

     More details

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

  161. Completion after Program Inversion of Injective Functions Reviewed

    Naoki Nishida and Masahiko Sakai

    Electronic Notes in Theoretical Computer Science   Vol. 237   page: 39-56   2009.4

     More details

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

    Given a constructor term rewriting system that defines injective functions, the inversion compiler proposed
    by Nishida, Sakai and Sakabe generates a conditional term rewriting system that defines the inverse relations
    of the injective functions, and then the compiler unravels the conditional system into an unconditional term
    rewriting system. In general, the resulting unconditional system is not (innermost-)confluent even if the
    conditional system is (innermost-)confluent. In this paper, we propose a modification of the Knuth-Bendix
    completion procedure, which is used as a post-processor of the inversion compiler. Given a confluent and
    operationally terminating conditional system, the procedure takes the resulting unconditional systems as
    input. When the procedure halts successfully, it returns convergent systems that are computationally
    equivalent to the conditional systems. To adapt the modified procedure to the conditional systems that are
    not confluent but innermost-confluent, we propose a simplified variant of the modified procedure. We report
    that the implementations of the procedures succeed in generating innermost-convergent inverse systems for
    all the examples we tried.

  162. Rewriting Induction for Constrained Term Rewriting Systems Reviewed

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

    IPSJ Transactions on Programming,   Vol. 2 ( 2 ) page: 80-96   2009.3

     More details

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

    The implicit induction, which is one of induction principles for proving inductive
    theorems of equational theories, has been extended to deal with constrained
    term rewriting systems. It has been applied to a method for proving equivalence
    of imperative programs. In this paper, we extend another induction principle,
    the rewriting induction, to cope with the case of constrained term rewriting
    systems, and show its correctness. We also propose a method for proving inductive
    theorems being based on the extended rewriting induction. Moreover,
    we show a technique to disprove inductive theorems.

  163. Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions

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

    IEICE Technical Report SS2008-44   Vol. 108 ( 362 ) page: 31-36   2008.12

     More details

    Language:Japanese  

  164. Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs

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

    IEICE Technical Report SS2008-45   Vol. 108 ( 362 ) page: 37-42   2008.12

     More details

    Language:English  

  165. Behavior Analysis of Scalable CAN Protocol on a Bit-Error Channel

    Kenji Ukai, Toshiki Sakabe, Hiroaki Takada, Ryo Kurachi, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2008-37   Vol. 108 ( 242 ) page: 61-66   2008.10

     More details

    Language:Japanese  

  166. 制約付き項書換え系における書換え帰納法

    坂田翼, 西田直樹, 坂部俊樹, 酒井, 正彦, 草刈圭一朗

    第71回情報処理学会・プログラミング研究会 配布資料     page: 1-12   2008.10

     More details

    Language:Japanese  

  167. A Preliminary Study on Behavior Analysis of Scalable CAN Protocol

    Kenji Ukai, Toshiki Sakabe, Hiroaki Takada, Ryo Kurachi, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    Record of 2008 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( O-262 ) page: 1   2008.9

     More details

    Language:Japanese  

  168. 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

     More details

    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.

  169. 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

     More details

    Authorship:Lead author   Language:English  

  170. 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

     More details

    Authorship:Lead author   Language:Japanese  

  171. 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

     More details

    Language:Japanese  

  172. 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

     More details

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

  173. 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

     More details

    Language:Japanese  

  174. 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

     More details

    Language:Japanese  

  175. 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

     More details

    Language:English  

  176. 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

     More details

    Language:Japanese  

  177. 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

     More details

    Language:Japanese  

  178. 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

     More details

    Language:Japanese  

  179. 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

     More details

    Language:Japanese  

  180. 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

     More details

    Language:Japanese  

  181. 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

     More details

    Language:Japanese  

  182. * 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

     More details

    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.

  183. 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

     More details

    Language:English  

  184. 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

     More details

    Language:Japanese  

  185. 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

     More details

    Authorship:Lead author   Language:English  

  186. 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

     More details

    Language:English  

  187. 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

     More details

    Language:English  

  188. Usable Rules and Labeling Product-Typed Terms for Dependency Pair Method in Simply-Typed Term Rewriting Systems Reviewed

    Takahiro Sakurai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

    The IEICE Transactions on Information and Systems   Vol. J90-D ( 4 ) page: 978-989   2007.4

     More details

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

  189. Automated Theorem Prover HOPSYS on Simply-Typed Rewriting Systems

    Akinori Kamada, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report SS2006-57   Vol. 106 ( 426 ) page: 7-12   2006.12

     More details

    Language:Japanese  

  190. Approach to Software Verification Based on Transformation from Procedural Programs to Rewrite Systems

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

    IEICE Technical Report SS2006-41 (KBSE2006-17)   Vol. 106 ( 324 ) page: 7-12   2006.10

     More details

    Language:Japanese  

  191. Example Programs Generated by GeneSys and Proposal of Introduction Rule

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

    IEICE Technical Report SS2006-46 (KBSE2006-22)   Vol. 106 ( 324 ) page: 37-42   2006.10

     More details

    Language:Japanese  

  192. Security Analysis of Information Flow for An Object-Oriented Language with Exception Handling

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

    IEICE Technical Report SS2006-42 (KBSE2006-18)   Vol. 106 ( 324 ) page: 13-18   2006.10

     More details

    Language:Japanese  

  193. Compiling Term Rewriting Systems Having Higher-Order Functions

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

    Record of 2006 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( O-437 ) page: 1   2006.9

     More details

    Language:Japanese  

  194. Unraveling for Conditional Term Rewriting Systems with Membership Constraints

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

    Record of 2006 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( O-438 ) page: 1   2006.9

     More details

    Language:Japanese  

  195. Transformation for Refining Unraveled Conditional Term Rewriting Systems Reviewed

    Naoki Nishida, Tomohiro Mizutani, and Masahiko Sakai

    Proceedings of the 6th International Workshop on Reduction Strategies in Rewriting and Programming (WRS'06)     page: 34-48   2006.8

     More details

    Authorship:Lead author   Language:English  

  196. Dependency Graph Method for Proving Termination of Narrowing Reviewed

    Naoki Nishida and Koichi Miura

    Proceedings of the 8th International Workshop on Termination (WST'06)     page: 12-16   2006.8

     More details

    Authorship:Lead author   Language:English  

  197. Transformation of Equational Rewriting Systems for Removing some Equations.

    Koichi Miura, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, and Keiichirou Kusakari

    IEICE Technical Report SS2006-14   Vol. 106 ( 120 ) page: 7-12   2006.6

     More details

    Language:Japanese  

  198. 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, and Naoki Nishida

    IEICE Technical Report SS2006-15   Vol. 106 ( 120 ) page: 13-18   2006.6

     More details

    Language:Japanese  

  199. Secrecy Verification of Spi Calculus Based on Term Regular Expressions

    Yoshihiko Tashiro, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2005-82   Vol. 105 ( 596 ) page: 35-40   2006.2

     More details

    Language:Japanese  

  200. Lexicographic Path Ordering for Proving Termination of Functional Programs

    Yumi Hoshino, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, and Naoki Nishida

    IEICE Technical Report SS2005-85   Vol. 105 ( 597 ) page: 13-18   2006.2

     More details

    Language:Japanese  

  201. Secrecy Verification by Transforming Cryptographic Protocol Descriptions to Coloured Petri Nets

    Daisuke Okuya, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2005-58   Vol. 105 ( 490 ) page: 19-24   2005.12

     More details

    Language:Japanese  

  202. Decidability of Termination for Left-Linear Shallow Term Rewriting Systems and Related

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

    IEICE Technical Report COMP2005-50   Vol. 105 ( 499 ) page: 9-13   2005.12

     More details

    Language:English  

  203. Type Judgement System for Communication Error in Distributed JoinJAVA Programs

    Masaki Saeki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2005-67   Vol. 105 ( 491 ) page: 25-30   2005.12

     More details

    Language:Japanese  

  204. On Completeness of Outermost Strategy for Overlapping TRSs

    Atsushi Iwata, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, and Toshiki Sakabe

    IEICE Technical Report SS2005-46   Vol. 105 ( 331 ) page: 39-44   2005.10

     More details

    Language:Japanese  

  205. Proving Sufficient Completeness of Functional Programs based on Recursive Structure Analysis and Strong Computability Reviewed

    Takahiro Sakurai, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the Forum on Information Technology 2005, Information Technology Letters   ( LA-001 ) page: 1-4   2005.9

     More details

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

  206. Type Judgement Systems for Assuring Distributed JoinJAVA Programs Run Normally

    Masaki Saeki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    Record of 2005 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( O-306 ) page: 1   2005.9

     More details

    Language:Japanese  

  207. Verifying Cryptographic Protocols by Using Coloured Petri Nets

    Daisuke Okuya, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    Record of 2005 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers   ( O-198 ) page: 1   2005.9

     More details

    Language:Japanese  

  208. Generation of Inverse Computation Programs of Constructor Term Rewriting Systems Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    the IEICE Transactions on Information and Systems   Vol. J88-D-I ( 8 ) page: 1171-1183   2005.8

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  209. Decidability of Termination for Semi-Constructor Term Rewriting Systems

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

    IEICE Technical Report SS2005-46   Vol. 105 ( 228 ) page: 13-18   2005.8

     More details

    Language:English  

  210. Programming Method in Obfuscated Language Malbolge

    Hisashi Iizawa, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, and Naoki Nishida

    IEICE Technical Report SS2005-22   Vol. 105 ( 129 ) page: 25-30   2005.6

     More details

    Language:Japanese  

  211. Dependency Graph Method for Proving Termination of Narrowing

    Koichi Miura, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, and Toshiki Sakabe

    IEICE Technical Report SS2005-23   Vol. 105 ( 129 ) page: 31-36   2005.6

     More details

    Language:Japanese  

  212. On Proving Termination of Simply-Typed Term Rewriting Systems Based on Strong Computability

    Keiichirou Kusakari, Takahiro Sakurai, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report SS2005-21   Vol. 105 ( 129 ) page: 19-24   2005.6

     More details

    Language:Japanese  

  213. Partial Inversion of Constructor Term Rewriting Systems Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 16th International Conference on Rewriting Techniques and Applications, Lecture Notes in Computer Science   Vol. 3467   page: 264-278   2005.4

     More details

    Authorship:Lead author   Language:English  

  214. On Recursion Removal from Non-Linear Top-Recursive Programs

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

    New Aspects of Theoretical Computer Science, RIMS Kokyuroku (LA Symposium 2004 Winter)   Vol. 1426   page: 39-44   2005.4

     More details

    Language:Japanese  

  215. 変換と部分評価に基づく非左辺正規なメタ項の停止性証明

    蛸島洋明, 酒井正彦, 坂部俊樹, 西田直樹, 草刈圭一朗

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   Vol. 1426   page: 113-118   2005.4

     More details

    Language:Japanese  

  216. 弱最内戦略を完全にする項書換え系の等価変換

    岡本晃治, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   Vol. 1426   page: 119-125   2005.4

     More details

    Language:Japanese  

  217. 到達可能性の判定における成長TRSに対する手法と正規化規則による手法の関係

    村田龍彦, 酒井正彦, 西田直樹, 草刈圭一朗, 坂部俊樹

    計算機科学基礎理論とその応用, 数理解析研究所講究録(2004年度冬のLAシンポジウム)   Vol. 1426   page: 106-112   2005.4

     More details

    Language:Japanese  

  218. Simulating Fusion Transformation by Program-Generation Transformation

    Masanori Nagashima, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, and Keiichirou Kusakari

    IEICE Technical Report SS2004-33   Vol. 104 ( 466 ) page: 43-48   2004.11

     More details

    Language:Japanese  

  219. On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report SS 2004-18   Vol. 104 ( 243 ) page: 25-30   2004.8

     More details

    Authorship:Lead author   Language:English  

  220. On Simulation-Completeness of Unraveling for Conditional Term Rewriting Systems

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    LA Symposium 2004 Summer   ( 7 ) page: 1-6   2004.7

     More details

    Authorship:Lead author   Language:English  

  221. Improving Efficiency of of Computation of Right-Linear Constructor Term Rewriting Systems with Extra Variables Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Computer Software   Vol. 21 ( 3 ) page: 40-47   2004.5

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  222. Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Electronic Notes in Theoretical Computer Science   Vol. 86 ( 3 ) page: 1-18   2003.11

     More details

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

  223. Computation Model of Term Rewriting Systems with Extra Variables Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Computer Software   Vol. 20 ( 5 ) page: 85-89   2003.9

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  224. Improving Efficiency of of Computation of Right-Linear Constructor Term Rewriting Systems with Extra Variables

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 20th Conference of Japan Society for Software Science and Technology (JSSST)   ( 5B-3 ) page: 1-5   2003.9

     More details

    Authorship:Lead author   Language:Japanese  

  225. Normal-form Computation by Left-most Innermost Narrowing on Right-Linear Overlay Term Rewriting Systems with Extra Variables

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    LA Symposium 2003 Summer   ( 24 ) page: 1-6   2003.7

     More details

    Authorship:Lead author   Language:Japanese  

  226. Narrowing-Based Simulation of Term Rewriting Systems with Extra Variables and its Termination Proof Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 12th International Workshop on Functional and (Constraint) Logic Programming (WFLP'03)     page: 198-211   2003.6

     More details

    Authorship:Lead author   Language:English  

  227. Narrowing-based Effective Rewriting and its Termination for Term Rewriting Systems with Extra Variables

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    New Aspects of Theoretical Computer Science, RIMS Kokyuroku (LA Symposium 2002 Winter)   Vol. 1325   page: 238-243   2003.5

     More details

    Authorship:Lead author   Language:Japanese  

  228. Narrowing-based Effective Rewriting and its Termination for Term Rewriting Systems with Extra Variables

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report COMP2003-68   Vol. 102 ( 593 ) page: 45-52   2003.1

     More details

    Authorship:Lead author   Language:Japanese  

  229. A Narrowing-based Reduction of Term Rewriting Systems with Extra Variables

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Record of 2002 Tokai-section Joint Conference of the Eight Institutes of Electrical and Related Engineers     page: 292   2002.9

     More details

    Authorship:Lead author   Language:Japanese  

  230. A Computation Model of Term Rewriting Systems with Extra Variables

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 19th Conference of Japan Society for Software Science and Technology (JSSST)   ( 6F-3 ) page: 1-5   2002.9

     More details

    Authorship:Lead author   Language:Japanese  

  231. Generation of a TRS Implementing the Inverses of Pure Treeless Functions Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Computer Software   Vol. 19 ( 1 ) page: 29-33   2002.1

     More details

    Authorship:Lead author   Language:Japanese   Publishing type:Research paper (scientific journal)  

  232. Generation of a TRS Implementing the Inverses of the Functions with Specified Arguments Fixed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report COMP2001-67   Vol. 101 ( 488 ) page: 33-40   2001.12

     More details

    Authorship:Lead author   Language:Japanese  

  233. Generation of Inverse Term Rewriting Systems for Pure Treeless Functions Reviewed

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the International Workshop on Rewriting in Proof and Computation (RPC'01)     page: 188-198   2001.10

     More details

    Authorship:Lead author   Language:English  

  234. Generation of a TRS Implementing the Inverses of Pure Treeless Functions

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    Proceedings of the 18th Conference of Japan Society for Software Science and Technology (JSSST)   ( 6C-3 ) page: 1-5   2001.9

     More details

    Authorship:Lead author   Language:Japanese  

  235. Generation of a Conditional TRS Implements the Inverses of Pure Treeless Functions

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report COMP2001-14   Vol. 101 ( 133 ) page: 9-16   2001.6

     More details

    Authorship:Lead author   Language:Japanese  

  236. Designing Unlimited Size Resource C-Libraries Freeing Users from GC Annoyance

    Naoki Nishida, Masahiko Sakai, and Toshiki Sakabe

    IEICE Technical Report SS2000-9   Vol. 100 ( 64 ) page: 25-32   2000.5

     More details

    Authorship:Lead author   Language:Japanese  

▼display all

Presentations 47

  1. A Sufficient Condition of Logically Constrained Term Rewrite Systems for Decidability of All-Path Reachability Problems with Constant Destinations

    Misaki Kojima and Naoki Nishida

    th 146th Workshop on IPSJ Special Interest Group on Programming  2023.10.31  IPSJ Special Interest Group on Programming

     More details

    Event date: 2023.10 - 2023.11

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Tokyo   Country:Japan  

  2. On Constrained Narrowing of Logically Constrained Term Rewrite Systems

    Naoki Nishida

    the 59th TRS Meeting  2023.9.28 

     More details

    Event date: 2023.9

    Language:English   Presentation type:Oral presentation (general)  

    Venue:New Welcity Izumo   Country:Japan  

  3. Unravelings and Narrowing Trees Towards Confluence of Deterministic CTRSs Invited International conference

    Naoki Nishida

    12th International Workshop on Confluence  2023.8.23  Cyrille Chenavier and Sarah Winkler

     More details

    Event date: 2023.8

    Language:English   Presentation type:Oral presentation (invited, special)  

    Venue:Obergurgl, Austria   Country:Austria  

  4. On Transforming Imperative Programs into LCTRSs via Injective Functions from Configurations to Terms

    Naoki Nishida

    the 57th TRS Meeting  2022.9.28 

     More details

    Event date: 2022.9

    Language:English   Presentation type:Oral presentation (general)  

    Venue:hybrid (Eiheiji / onlien)   Country:Japan  

  5. Inversion and Determinization in Term Rewriting Invited International conference

    Naoki Nishida

    the meeting of IFIP Working Group 1.6: Rewriting  2022.7.31  IFIP Working Group 1.6: Rewriting

     More details

    Event date: 2022.7

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Haifa, Israel   Country:Israel  

    As a transformational approach, inversion is formulated in several settings, and the basic ideas are naive and similar. To generate a better form, e.g., non-overlapping systems if possible, determinization is used as a post-process of inversion for injective functions, and is the most challenging part in developing an inversion framework. In this talk, I introduce a framework of inversion and determinization in term rewriting. First, I explain a direct inversion of deterministic CTRSs, and a direct MSV-based determinization. Next, I explain the framework proposed by Gluck and Kawabe, which uses context-free grammars as intermediate representations of CTRSs. Finally, I explain a framework based on context-free expressions.

  6. On Semantically Equivalent Operations for Inversion of DCTRSs

    Naoki Nishida

    the 56th TRS Meeting  2022.2.24 

     More details

    Event date: 2022.2

    Language:English   Presentation type:Oral presentation (general)  

    Venue:hybrid (Nagoya University / onlien)   Country:Japan  

  7. On Improving Confluence and Infeasibility Proofs in CO3

    Naoki Nishida

    the 55th TRS Meeting  2021.9.29 

     More details

    Event date: 2021.9

    Language:English   Presentation type:Oral presentation (general)  

    Venue:online   Country:Japan  

  8. Transformation of Concurrent Programs with Semaphores into LCTRSs

    Naoki Nishida

    the 54th TRS Meeting  2021.3.16 

     More details

    Event date: 2021.3

    Language:English   Presentation type:Oral presentation (general)  

    Venue:online   Country:Japan  

  9. Proving Infeasibility by Basic Narrowing

    Naoki Nishida

    the 50th TRS Meeting 

     More details

    Event date: 2019.2 - 2019.3

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Ikaho, Gunma   Country:Japan  

  10. Proving Infeasibility by Narrowing Trees

    Naoki Nishida

    the 49th TRS Meeting 

     More details

    Event date: 2018.9

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Ikaho, Gunma   Country:Japan  

  11. 組合せ最適化問題を記述するための関係代数の集合上への拡張

    坂梨元軌,酒井正彦,西田直樹,橋本健二

    第20回プログラミングおよびプログラミング言語ワークショップ 

     More details

    Event date: 2018.3

    Language:Japanese   Presentation type:Poster presentation  

    Venue:皆生グランドホテル天水   Country:Japan  

    組合せ最適化問題は様々な分野に応用できるが,効率良く解くためには専門知識を必要とするという問題がある.本研究では,組合せ最適化問題を簡潔に記述できなおかつ効率的に解くことができるシステムの構築を目指して,理論的な枠組として関係の集合上に拡張した関係代数を提案し,それに基づく拡張SQL構文とその汎用ソルバによる解法を議論する.

  12. 配列を含むC言語サブセットから難解言語Malbolgeへのコンパイラ

    岩金カナン,坂梨元軌,酒井正彦,西田直樹,橋本健二

    第20回プログラミングおよびプログラミング言語ワークショップ 

     More details

    Event date: 2018.3

    Language:Japanese   Presentation type:Poster presentation  

    Venue:皆生グランドホテル天水   Country:Japan  

    難解プログラミング言語とは意図的に読解が困難になるように設計された言語であり、中でも難解な言語としてMalbolgeがある。現在では低級アセンブリ言語と制御付き疑似命令列を経てC言語に制限を設けた高級言語からのコンパイラが実現されている。しかしこの高級言語では配列を扱うことができず、複雑なプログラムが書けなかった。本研究では配列を含む高級言語を処理してMalbolgeへ変換する手法を実装した。この変換にはメモリの空き領域をスタックとして用いることで実現した。

  13. From Dependency Chains to Bounded Monotone Sequences of Integers

    Naoki Nishida

    the 47th TRS Meeting 

     More details

    Event date: 2017.9

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Matsue, Shimane   Country:Japan  

  14. On Proving Infeasibility of Conditional Critical Pairs via Narrowing Trees

    Naoki Nishida

    the 46th TRS Meeting 

     More details

    Event date: 2017.2 - 2017.3

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Shinojima, Aichi   Country:Japan  

  15. Heuristics for Proving Termination of Constrained Rewriting Systems via Rule Duplication International conference

    Naoki Nishida

    4th Austria - Japan Summer Workshop on Term Rewriting 

     More details

    Event date: 2016.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:Austria  

  16. On Uninterpreted Functions in Proving Termination of Constrained Rewriting

    Naoki Nishida

    the 41st TRS Meeting 

     More details

    Event date: 2014.9

    Language:English   Presentation type:Oral presentation (general)  

    Venue:Jozankei, Sapporo   Country:Japan  

  17. On Soundness for Reduction of TRSs Obtained by Condition Elimination for Normal CTRSs

    Naoki Nishida

    the 40th TRS Meeting 

     More details

    Event date: 2014.3

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  18. A Finite Representation of the Narrowing Space and its Application International conference

    Naoki Nishida

    COMPUTER SCIENCE COLLOQUIUM, IMADA, University of Southern Denmark 

     More details

    Event date: 2014.3

    Language:English  

    Country:Denmark  

  19. Automated Verification of C Programs via Rewriting Induction of Constrained TRSs International conference

    Naoki Nishida

    Seminar at Research Group "Verification meets Algorithm Engineering", the Institute for Theoretical Computer Science, Karlsruhe Institute of Technology 

     More details

    Event date: 2013.7

    Language:English   Presentation type:Oral presentation (invited, special)  

    Country:Germany  

    In this talk, we introduce an automated theorem proving method based on rewriting induction of constrained TRSs, and show how to apply it to the verification of C programs over integers. Especially, we show a technique to automatically generate (a candidate of) lamma equations that are necessary for the proof.

  20. Computing More Specific Versions of Conditional Rewriting Systems

    Naoki Nishida

    the 37th TRS Meeting 

     More details

    Event date: 2012.11

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  21. Program Inversion and MSV Transformation in Term Rewriting International conference

    Naoki Nishida

    Master Seminar 1, Institute of Computer Science, University of Innsbruck 

     More details

    Event date: 2012.10

    Language:English   Presentation type:Oral presentation (general)  

    Country:Austria  

    In this talk, I present two principles of program inversion
    in term rewriting setting, a classical one and another one for tail
    recursion. Rewrite rules generated by inversion methods based on the
    principles are often non-deterministic w.r.t. application of rules to
    redexes even if given functions are injective. For this reason,
    determinization of inverted programs is one of the most challenging
    topics in program inversion of injective functions. To make inverted
    programs deterministic, I present an MSV transformation of term
    rewriting systems, which converts a rewrite system to a more specific
    version. The notion of MSV originated from the context of logic
    programs.

  22. Program Inversion for Tail Recursive Functions International conference

    Naoki Nishida

    Seminar at DSIC, Technical University of Valencia 

     More details

    Event date: 2011.12

    Language:English   Presentation type:Oral presentation (invited, special)  

    Country:Spain  

  23. Disproving and Postulating for Multi-Context Rewriting Induction

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

    the 28th Conference of Japan Society for Software Science and Technology 

     More details

    Event date: 2011.9

    Language:Japanese   Presentation type:Poster presentation  

    Country:Japan  

  24. On Soundness of CTRS Transformations

    Naoki Nishida

    the 35th TRS Meeting 

     More details

    Event date: 2011.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  25. On Verifying Equivalence between Functions in Constrained TRSs via Tree Homomorphisms

    Naoki Nishida

    the 35th TRS Meeting 

     More details

    Event date: 2011.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  26. 難解言語Malbolgeにおける高級アセンブリ言語への加算命令の追加

    安藤 聡, 長坂 哲, 酒井 正彦, 坂部 俊樹, 草刈 圭一朗, 西田 直樹

    第13回プログラミングおよびプログラミング言語ワークショップ 

     More details

    Event date: 2011.3

    Language:Japanese   Presentation type:Poster presentation  

    Venue:定山渓ビューホテル   Country:Japan  

  27. 難解言語Malbolgeにおけるプログラミング環境の構築と改良

    長坂 哲, 安藤 聡, 酒井 正彦, 坂部 俊樹, 草刈 圭一朗, 西田 直樹

    第13回プログラミングおよびプログラミング言語ワークショップ 

     More details

    Event date: 2011.3

    Language:Japanese   Presentation type:Poster presentation  

    Venue:定山渓ビューホテル   Country:Japan  

  28. 制約付き項書換え系における木準同型写像を用いた等価性検証ツール

    高桑 一也, 西田 直樹, 大場 康司, 酒井 正彦, 坂部 俊樹, 草刈 圭一朗

    第13回プログラミングおよびプログラミング言語ワークショップ 

     More details

    Event date: 2011.3

    Language:Japanese   Presentation type:Poster presentation  

    Venue:定山渓ビューホテル   Country:Japan  

  29. On Inverting Tail Recursive Functions

    Naoki Nishida

    the 34th TRS Meeting 

     More details

    Event date: 2011.2

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  30. 例外処理を持つ関数型プログラムの停止性証明法

    馬場正貴, 酒井正彦, 濱口毅, 西田直樹, 坂部俊樹, 草刈圭一朗

    第12回プログラミングおよびプログラミング言語ワークショップ 

     More details

    Event date: 2010.3

    Language:Japanese   Presentation type:Poster presentation  

    Country:Japan  

  31. SATソルバを利用したお絵かきロジックの問題作成支援ツール

    長坂哲, 伊藤寛之, 酒井正彦, 草刈圭一朗, 西田直樹, 坂部俊樹

    組合せゲーム・パズル ミニプロジェクト 第5回ミニ研究集会 

     More details

    Event date: 2010.3

    Language:Japanese   Presentation type:Oral presentation (general)  

    Country:Japan  

  32. On Improving Lemma Generation Framework for Constrained Term Rewriting Systems

    the 33rd TRS Meeting 

     More details

    Event date: 2010.2

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  33. On Automating Theorem Proving for Constrained Equations

    the 32nd TRS Meeting 

     More details

    Event date: 2009.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  34. Prototype of Automated Theorem Prover for Constrained Equations

    the 26th Conference of Japan Society for Software Science and Technology 

     More details

    Event date: 2009.9

    Language:Japanese   Presentation type:Poster presentation  

    Country:Japan  

  35. Approach to Procedural-Program Verification Based on Implicit Induction

    th 68th Workshop on IPSJ Special Interest Group on Programming 

     More details

    Event date: 2008.3

    Language:Japanese  

    Country:Japan  

  36. Comparison of Unraveling Techniques for Deterministic Conditional Term Rewriting Systems International conference

    2nd Austria - Japan Summer Workshop on Term Rewriting 

     More details

    Event date: 2007.8

    Language:English   Presentation type:Oral presentation (general)  

  37. Convergent Term Rewriting Systems for Computing Inverses of Injective Functions

    the 28th TRS Meeting 

     More details

    Event date: 2007.2

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  38. On Reachability of Oriented Conditional Term Rewriting Systems

    the 27th TRS Meeting 

     More details

    Event date: 2006.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  39. Improving Unraveling for Deterministic Conditional Term Rewriting Systems

    the 26th TRS Meeting 

     More details

    Event date: 2006.2

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  40. Dependency Graph Method for Proving Termination of Narrowing International conference

    Austria - Japan Summer Workshop on Term Rewriting 

     More details

    Event date: 2005.8

    Language:English   Presentation type:Oral presentation (general)  

  41. Partial Inversion of Constructor Term Rewriting Systems

    the 25th TRS Meeting 

     More details

    Event date: 2004.11

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  42. Transformational Approach to Inverse Computation in Term Rewriting

    the 18th Tokyo Programming Seminar (ToPS) 

     More details

    Event date: 2004.10

    Language:English   Presentation type:Oral presentation (invited, special)  

    Country:Japan  

  43. Completeness of Unraveling Transformation for Left-Linear Conditional Term Rewriting Systems

    the 24th TRS Meeting 

     More details

    Event date: 2004.4

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  44. Basic Narrowing Improves Efficiency of Computation of Right-Linear Term Rewriting Systems with Extra Variables

    the 23rd TRS Meeting 

     More details

    Event date: 2003.9

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  45. Condition for Generation of Terminating Inverse TRSs from Constructor TRSs

    the 22nd TRS Meeting 

     More details

    Event date: 2003.3

    Language:English   Presentation type:Oral presentation (general)  

    Country:Japan  

  46. Narrowing-Based Reduction of Term Rewriting Systems with Extra Variables

    the 21st TRS Meeting 

     More details

    Event date: 2002.10

    Language:English   Presentation type:Oral presentation (general)  

  47. On Generating Inverse Systems of Constructor TRSs

    the 20th TRS Meeting 

     More details

    Event date: 2002.3

    Language:English   Presentation type:Oral presentation (general)  

▼display all

Research Project for Joint Research, Competitive Funding, etc. 5

  1. 組込み制御システムの検証手法に関する研究

    2019.4 - 2020.3

    学内共同研究 

  2. 組込み制御システムの検証手法に関する研究

    2017.9 - 2019.3

    学内共同研究 

  3. 組込み制御システムの検証手法に関する研究

    2016.9 - 2017.8

    学内共同研究 

  4. 左線形構成子項書換え系におけるナローイング計算の停止性証明の手法に関する研究

    2009.9

    研究等助成(海外渡航援助) 

      More details

    Grant type:Competitive

  5. 条件付き項書換え系から等価な条件無し項書換え系への変換とその応用に関する研究

    2007.4 - 2009.3

    栢森情報科学振興財団研究助成金 

      More details

    Grant type:Competitive

KAKENHI (Grants-in-Aid for Scientific Research) 7

  1. 書換え帰納法を利用したプログラム等価性検証技術の開発

    2018.4 - 2023.3

    科学研究費補助金  基盤研究(C)

    西田直樹

      More details

    Authorship:Principal investigator 

    本研究では制約付き項書換えシステムに対する書換え帰納法に基づく定理自動証明ツールを開発し,命令型プログラミング言語のプログラム等価性検証の新たな手法の確立をめざす.具体的には,関数型プログラミング言語だけでなく命令型プログラミング言語の計算モデルとしての利用を期待できる制約付き項書換えシステムに対する書換え帰納法に基づく帰納的定理証明法を命令型プログラミング言語から得られた書換えシステム向けに自動化することで,命令型プログラム向けの定理自動証明ツールを開発する.特に,関数の等価性など等式で表現できる性質の検証への応用をめざす.命令型プログラム向けの自動化を実現するために,書換え帰納法の推論規則の適用戦略の改良,補題等式の生成法の開発に取り組む.また,不等式も同時に扱う,等式付き書換えに対応するなど理論の拡張にも取り組む.

  2. 実時間性を持つ並行プログラムに対するデバッグのための逆方向計算モデル

    2017.4 - 2021.3

    科学研究費補助金  基盤研究(B)

    結縁 祥治

      More details

    Authorship:Coinvestigator(s) 

  3. 単射性を持つ関数型プログラムの逆計算プログラム生成に関する研究

    2009.4 - 2013.3

    科学研究費補助金  若手研究(B)

    西田直樹

      More details

    Authorship:Principal investigator 

  4. 高階関数プログラムの停止性判定に関する研究

    2008.4 - 2012.3

    科学研究費補助金  基盤研究(C)

    草刈圭一朗

      More details

    Authorship:Coinvestigator(s) 

  5. 関数型プログラムの逆計算プログラム生成に関する研究

    2005.4 - 2008.3

    科学研究費補助金  若手研究(B)

    西田 直樹

      More details

    Authorship:Principal investigator 

  6. 書換えに基づく例外型を持つオブジェクト指向プログラムの型推論

    2004.4 - 2008.3

    科学研究費補助金  基盤研究(B)

    坂部俊樹

      More details

    Authorship:Coinvestigator(s) 

  7. 関数型言語の解析・検証・効率的実行のための書換え理論の研究

    2003.4 - 2010.3

    科学研究費補助金  基盤研究(C)

    酒井正彦

      More details

    Authorship:Coinvestigator(s) 

▼display all

 

Teaching Experience (On-campus) 38

  1. 計算論基礎特論A

    2022

  2. Algorithm 2

    2022

  3. Algorithm 1

    2022

  4. First Year Seminar B

    2020

  5. Algorithm 2

    2020

  6. Algorithm 1

    2020

  7. 計算論基礎特論A

    2020

  8. 基礎セミナー

    2019

  9. 計算モデル特論

    2019

  10. Algorithm 2

    2019

  11. Algorithm 1

    2019

  12. アルゴリズム及び演習

    2018

  13. Algorithm 2

    2018

  14. Algorithm 1

    2018

  15. Basic Topic in Theory of Computation A

    2018

  16. 計算モデル特論

    2017

  17. 基礎セミナー

    2017

  18. アルゴリズム及び演習

    2017

  19. 基礎セミナー

    2016

  20. Foundation of Software

    2016

  21. アルゴリズム及び演習

    2016

  22. アルゴリズム及び演習

    2015

  23. Foundation of Software

    2015

  24. Foundation of Software

    2014

  25. 電気・電子・情報工学序論

    2014

  26. 計算機プログラミング基礎及び演習

    2014

  27. 基礎セミナー

    2014

  28. 電気・電子・情報工学序論

    2013

  29. 計算機プログラミング基礎及び演習

    2013

  30. 基礎セミナー

    2013

  31. コンパイラおよび演習

    2012

  32. プログラミングおよび演習

    2012

  33. 情報工学実験第2

    2012

  34. 情報工学実験第1

    2012

  35. 情報基礎論第1および演習

    2011

  36. 情報工学実験第2

    2011

  37. 情報工学実験第1

    2011

  38. プログラミングおよび演習

    2011

▼display all