Committee 
Date Time 
Place 
Paper Title / Authors 
Abstract 
Paper # 
SS 
20150310 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.) SS201469 
Unfold/Fold transformations have been widely used for program transformation, theorem proving, and so on.
Unfold and Fo... [more] 
SS201469 pp.8590 
SS 
20150310 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.) SS201470 
In proving equations to be inductive theorems of constrained term rewriting systems, we often need appropriate lemmas of... [more] 
SS201470 pp.9196 
MSS, SS 
20150126 16:55 
Tottori 

On Efficacy of Narrowing in Proving Termination of Constrained Term Rewriting Systems Tomoya Ueyama, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) MSS201476 SS201440 
[more] 
MSS201476 SS201440 pp.4348 
MSS, SS 
20150126 17:45 
Tottori 

Implementing a Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling Koichi Ota, Takeshi Hamaguchi, Masahiko Sakai (Nagoya Univ.), Akihisa Yamada (AIST), Naoki Nishida, Toshiki Sakabe (Nagoya Univ.) MSS201478 SS201442 
In this paper, we discuss implementation of the conditional dependency pair method for proving termination of functional... [more] 
MSS201478 SS201442 pp.5560 
KBSE, SS, IPSJSE [detail] 
20140710 16:20 
Hokkaido 
FuranoBunkaKaikan 
Deciding Code Allocation on Malbolge LowLevel Assembler Tatsuki Kato, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) SS201418 KBSE201421 
Malbolge is known as one of the most esoteric and hardtoprogramming languages.
Recently a lowlevel assembler (LAas... [more] 
SS201418 KBSE201421 pp.99104 
SS 
20140311 13:30 
Okinawa 
Tenbusu Naha 
On Detecting Useless Transition Rules of Constrained Tree Automata Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Kenji Hashimoto (Nagoya Univ.) SS201377 
Reduction completeness of terms is proved many times in a theorem proving method for constrained term rewriting systems ... [more] 
SS201377 pp.3136 
SS, KBSE 
20130726 10:30 
Hokkaido 

Malbolge with 20trits word length and its programming Tatsuki Kato, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS201325 KBSE201325 
Malbolge is known to be one of the most esoteric programming languages.
Recently a lowlevel assembly language (LAlang... [more] 
SS201325 KBSE201325 pp.7378 
MSS, SS 
20130307 11:40 
Fukuoka 
Shikanoshima 
On Composing the Simplex Method and Gomory Cut for Deriving Integer Assignments Masaaki Fushimi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) MSS201278 SS201278 
The simplex method is one of the methods to derive rational assignments from linear constraints on ratiolals. It is know... [more] 
MSS201278 SS201278 pp.109114 
SS 
20130110 13:30 
Okinawa 

Construction of Constrained Tree Automata Recognizing Ground Instances of Constrained Terms Yasuhiro Nakano, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) 
A theorem proving method for constrained term rewriting systems, which is based on rewriting induction, needs a decision... [more] 
SS201247 pp.712 
SS 
20130110 15:15 
Okinawa 

Using SAT Solvers for Solving ControlInstruction Layout Problems in LowLevel Assembly Programming for Malbolge Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) 
Malbolge is known as one of the most esoteric programming languages. Although it became possible to write programs in M... [more] 
SS201250 pp.2530 
SS, IPSJSE 
20121101 10:25 
Hiroshima 
Hiroshima City University 
A SAT Encoding for Finding Operation Sequences of Malbolge that Implement Tritwise Functions Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS201237 
Malbolge is known to be one of the most esoteric programming languages. Although it becomes possible to write programs i... [more] 
SS201237 pp.712 
KBSE, SS 
20120728 13:10 
Hokkaido 
Future University Hakodate 
On Extending Matching Operation in Grammar Programs for Program Inversion Minami Niwa, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS201227 KBSE201229 
[more] 
SS201227 KBSE201229 pp.103108 
SS 
20120511 10:45 
Ehime 
Ehime Univ. 
Introducing Array Mechanism into HighLevel Assembly Language for Malbolge Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS20128 
Malbolge is known to be one of the most esoteric programming languages. Although it is possible to write programs in Mal... [more] 
SS20128 pp.4348 
SS, MSS 
20120126 14:15 
Kochi 
Kochi City CulturePlaza CulPort 
Automatic Generation of Nonlinear Loop Invariants for Programs with Function Calls Eiichi Suzuki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) MSS201161 SS201146 
Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automat... [more] 
MSS201161 SS201146 pp.3944 
SS, MSS 
20120126 14:45 
Kochi 
Kochi City CulturePlaza CulPort 
On class of equation sets whose word problems are reducible to those of ground equation sets Toshimitsu Sakai, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari (Nagoya Univ.) MSS201162 SS201147 
The word problem of an equation set is to decide, given two terms, whether the two terms are equivalent under the equati... [more] 
MSS201162 SS201147 pp.4549 
SS, MSS 
20120126 15:30 
Kochi 
Kochi City CulturePlaza CulPort 
On Rewriting Induction for Simplytyped Term Rewriting Systems Akira Ozeki, Keiichirou Kusakari, Tsubasa Sakata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) MSS201163 SS201148 
Rewriting induction is a principle of proving inductive theorems by means of derivations obtained by applying inference ... [more] 
MSS201163 SS201148 pp.5156 
SS, MSS 
20120126 16:00 
Kochi 
Kochi City CulturePlaza CulPort 
On Usable Rules under Argument Filterings in HigherOrder Rewrite Systems Kazuhiro Ooi, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) MSS201164 SS201149 
The static dependency pair method is known as a powerful method for proving termination of higherorder rewrite systems ... [more] 
MSS201164 SS201149 pp.5762 
SS 
20111028 12:15 
Ishikawa 
JAIST 
Incorporating Elementary Symmetric Clauses into SAT Solvers with TwoWatchedLiteral Scheme Yoshizane Hino, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS201138 
Umano et al.\ introduced elementary symmetric clauses (ESclauses) into CNF formula in 2010 as a method for improving SA... [more] 
SS201138 pp.6772 
SS 
20110307 14:45 
Okinawa 
Okinawaken Seinen Kaikan 
Tree Automata with Constraints and their ClosureProperties Katsuhisa Kurahashi, Masahiko Sakai, Naoki Nishida, Futoshi Nomura, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS201063 
Tree automata are useful in analyzing properties of term rewriting systems since the class of recognizable tree language... [more] 
SS201063 pp.6166 
SS 
20101214 16:20 
Gunma 
IkahoOnsen Hotel Tenbo 
On nontermination proof of rightlinear and rightshallow term rewriting systems based on forward narrowing Tatsuya Hattori, Masahiko Sakai, Naoki Nishida, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) SS201044 
Detecting nontermination of term rewriting systems based on forward narrowing is used in termination tools such as APro... [more] 
SS201044 pp.3136 