Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
SS |
2023-03-15 09:30 |
Okinawa |
(Okinawa, Online) (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. (Nagasaki, Online) (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 |
HIP |
2021-09-17 10:55 |
Online |
Online (Zoom) (Online) |
Beverage's preference estimation based on emotional reaction and EEG activity Kuangzhe Xu (KGU), Kenji Katahira (WU), Yoichi Yamazaki, zhang fan, Naoki Nishida, Yuichiro Tamai (KGU), Naoyuki Matsuzaki (Suntory Global Innovation Center), Noriko Nagata (KGU) HIP2021-27 |
In recent years, many studies have tried to quantify Kansei values and found that human psychological and physiological ... [more] |
HIP2021-27 pp.31-36 |
MSS, SS |
2021-01-27 15:00 |
Online |
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 |
(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. (Kumamoto) |
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 |
(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 |
(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 |
(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 |
(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 |
(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 |
(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 |
(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 |
(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 |
(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 |
(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 (Ishikawa) |
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 (Ishikawa) |
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 |
(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 (Okinawa) |
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 |