| IEICE Technical Committee Submission System Conference Schedule |
Online Proceedings [Sign in] Tech. Rep. Archives |
All Technical Committee Conferences (Searched in: All Years)
| Committee | Date Time | Place | Paper Title / Authors | Abstract | Paper # | |
| SS | 2023-03-15 09:30 |
Okinawa | (Primary: On-site, Secondary: Online) |
On Polynomial Interpretations Toward Termination of Logically Constrained Term Rewrite Systems with Bit Vector Arithmetic Ayuka Matsumi, Naoki Nishida, Misaki Kojima, Donghoon Shin (Nagoya Univ.)  SS2022-61 |
Logically constrained term rewrite systems with the bit-vector theory (BV-LCTRSs, for short) are useful as models of pro... [more] | SS2022-61 pp.85-90 |
| SS, MSS | 2022-01-12 09:40 |
Nagasaki | Nagasakiken-Kensetsu-Sogo-Kaikan Bldg. (Primary: On-site, Secondary: Online) |
On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR Takumi Kato, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2021-47 SS2021-34 |
A method to verify programs written in a simple C-like language via logically constrained term rewrite systems (LCTRS, f... [more] | MSS2021-47 SS2021-34 pp.89-94 |
| MSS, SS | 2021-01-27 15:00 |
Online | Online | Speeding up combinatorial optimization solver CombSQL+ by introducing Pseudo-Boolean constraints Junichiro Kishi, Masahiko Sakai, Naoki Nishida, Kenji Hashimoto (Nagoya univ.) MSS2020-40 SS2020-25 |
The authors have proposed a solver CombSQL+ for combinatorial optimization problems (COPs) described in extended SQL lan... [more] | MSS2020-40 SS2020-25 pp.66-71 |
| SS | 2020-03-04 15:10 |
Okinawa | (Cancelled but technical report was issued) |
Transforming Programs with Exclusive Control into Logically Constrained Term Rewrite Systems Misaki Kojima, Naoki Nishida, Yutaka Matsubara, Masahiko Sakai (Nagoya Univ.) SS2019-46 |
To apply Logically Constrained Term Rewrite Systems (LCTRSs, for short) to program verification, a previous work targets... [more] | SS2019-46 pp.31-36 |
| DC, SS | 2019-10-24 14:55 |
Kumamoto | Kumamoto Univ. | Extending rewriting induction to existentially quantified equations Kazushi Nishie, Naoki Nishida, Masahiko sakai (Nagoya Univ.) SS2019-17 DC2019-45 |
In this paper, we extend rewriting induction which is developed to prove equations, to existentially quantified equation... [more] | SS2019-17 DC2019-45 pp.25-30 |
| SS | 2019-03-04 16:45 |
Okinawa | SQL queries for generating input constraints of SMT solvers from descriptions of combinatorial optimization problems Genki Sakanashi, Masahiko Sakai, Naoki Nishida, Kenji Hashimoto (Nagoya Univ.) SS2018-66 |
The authors recently proposed an SQL-based language CombSQL+ for specifying combinatorial optimization problems, and sho... [more] | SS2018-66 pp.85-90 |
|
| MSS, SS | 2019-01-16 09:25 |
Okinawa | On Representation of Structures and Unions in Logically Constrained Rewriting Yoshiaki Kanazawa, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2018-67 SS2018-38 |
Recently, several methods for verifying imperative programs by means of transformations into term rewriting systems have... [more] | MSS2018-67 SS2018-38 pp.67-72 |
|
| MSS, SS | 2019-01-16 09:50 |
Okinawa | Extending Narrowing Trees to Basic Narrowing in Term Rewriting Yuya Maeda, Naoki Nishida, Masahiko Sakai, Tomoya Kobayashi (Nagoya Univ.) MSS2018-68 SS2018-39 |
Narrowing computation of a term rewriting system is an extension of rewriting by replacing matching with unification, wh... [more] | MSS2018-68 SS2018-39 pp.73-78 |
|
| MSS, NLP (Joint) |
2018-03-13 10:20 |
Osaka | Minimum Potential Model for the Dripping Faucet Chaos Naoki Nishida, Ken Kiyono (Osaka Univ.) NLP2017-101 |
The mechanism of deterministic chaos observed in a dripping water faucet has been investigated. In the previous studies,... [more] | NLP2017-101 pp.1-4 |
|
| SS, KBSE, IPSJ-SE [detail] | 2017-07-20 15:50 |
Hokkaido | Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergers Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, Tomoya Ueyama (Nagoya Univ.) SS2017-17 KBSE2017-17 |
In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations t... [more] | SS2017-17 KBSE2017-17 pp.139-144 |
|
| SS, KBSE, IPSJ-SE [detail] | 2017-07-20 16:15 |
Hokkaido | A compiler that translates to Malbolge from a C-language subset containing recursive calls Genki Sakanashi, Shohei Kobe, Masahiko Sakai, Naoki Nishida, Kenji Hashimoto (Nagoya Univ.) SS2017-18 KBSE2017-18 |
Malbolge is an esoteric programming language, which is promising to protect intellectual property rights due to its diff... [more] | SS2017-18 KBSE2017-18 pp.145-150 |
|
| SS | 2017-03-10 10:45 |
Okinawa | Proving Confluence of Hierarchical Conditional Term Rewriting Systems without Sufficient Completeness Takayuki Kuroda, Naoki Nishida, Hiroyuki Seki (Nagoya Univ.) SS2016-77 |
A transformational approach to confluence proofs for conditional term rewriting systems (CTRS) has been investigated, bu... [more] | SS2016-77 pp.103-108 |
|
| KBSE, SS, IPSJ-SE [detail] | 2016-07-14 13:40 |
Hokkaido | An intermediate language for a compiler generating highly obfuscated Malbolge codes Shohei Kobe, Masahiko Sakai, Naoki Nishida, Hiroyuki Seki (Nagoya Univ.) SS2016-12 KBSE2016-18 |
[more] | SS2016-12 KBSE2016-18 pp.105-110 |
|
| SS | 2016-03-10 10:50 |
Okinawa | An extension of SQL for specifying combinatorial optimization problems Yusaku Uchida, Masahiko Sakai, Naoki Nishida (Nagoya Univ.) SS2015-80 |
The performance of satisfiability (SAT) solvers have incredibly improved in recent years. It is, however, difficult to ... [more] |
SS2015-80 pp.25-30 |
|
| SS | 2016-03-10 11:15 |
Okinawa | Program Verification Using Non-linear Loop Invariants Generated by Partially Applying an Extended Farkas' Lemma Makishi Yanagisawa, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) SS2015-81 |
To generate loop invariants, methods that, using Farkas' lemma, convert verification formulas obtained from a given temp... [more] | SS2015-81 pp.31-36 |
|
| SS, MSS | 2016-01-25 16:45 |
Ishikawa | Shiinoki-Geihin-Kan | On Proving Termination and Inductive Theorems Simultaneously for Constrained Term Rewriting Systems Yoshifumi Kawamoto, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2015-48 SS2015-57 |
[more] | MSS2015-48 SS2015-57 pp.75-80 |
| SS, MSS | 2016-01-26 11:05 |
Ishikawa | Shiinoki-Geihin-Kan | Transforming Constrained Dependency Pairs by Narrowing Tomohiro Sasano, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2015-57 SS2015-66 |
The dependency pair framework, a method for proving termination of term rewriting systems, has been extended for constra... [more] | MSS2015-57 SS2015-66 pp.123-128 |
| KBSE, SS, IPSJ-SE [detail] | 2015-07-24 11:10 |
Hokkaido | An Equivalent Transformation of Constrained Term Rewriting Systems by Pattern Elimination Takahiro Nagao, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) SS2015-33 KBSE2015-26 |
A constrained term rewriting system, an extension of term rewriting systems, can control application of rules by constra... [more] | SS2015-33 KBSE2015-26 pp.167-172 |
|
| SS | 2015-03-10 09:30 |
Okinawa | OKINAWAKEN SEINENKAIKAN | A Heuristic to Solve Inverse Unfolding Problem for Functions Dealing with Tree Structure Data Tomofumi Kato, Masanori Nagashima, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe (Nagoya Univ.) SS2014-69 |
Unfold/Fold transformations have been widely used for program transformation, theorem proving, and so on. Unfold and Fo... [more] |
SS2014-69 pp.85-90 |
| SS | 2015-03-10 09:55 |
Okinawa | OKINAWAKEN SEINENKAIKAN | Heuristics for Automatically Proving Commutativity of Function Composition for Constrained Term Rewriting Systems Ryutaro Kuriki, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) SS2014-70 |
In proving equations to be inductive theorems of constrained term rewriting systems, we often need appropriate lemmas of... [more] | SS2014-70 pp.91-96 |
[Return to Top Page]