Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
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 |
MSS, SS |
2015-01-26 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.) MSS2014-76 SS2014-40 |
[more] |
MSS2014-76 SS2014-40 pp.43-48 |
MSS, SS |
2015-01-26 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.) MSS2014-78 SS2014-42 |
In this paper, we discuss implementation of the conditional dependency pair method for proving termination of functional... [more] |
MSS2014-78 SS2014-42 pp.55-60 |
KBSE, SS, IPSJ-SE [detail] |
2014-07-10 16:20 |
Hokkaido |
Furano-Bunka-Kaikan |
Deciding Code Allocation on Malbolge Low-Level Assembler Tatsuki Kato, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) SS2014-18 KBSE2014-21 |
Malbolge is known as one of the most esoteric and hard-to-programming languages.
Recently a low-level assembler (LA-as... [more] |
SS2014-18 KBSE2014-21 pp.99-104 |
SS |
2014-03-11 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.) SS2013-77 |
Reduction completeness of terms is proved many times in a theorem proving method for constrained term rewriting systems ... [more] |
SS2013-77 pp.31-36 |
SS, KBSE |
2013-07-26 10:30 |
Hokkaido |
|
Malbolge with 20trits word length and its programming Tatsuki Kato, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2013-25 KBSE2013-25 |
Malbolge is known to be one of the most esoteric programming languages.
Recently a low-level assembly language (LA-lang... [more] |
SS2013-25 KBSE2013-25 pp.73-78 |
MSS, SS |
2013-03-07 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.) MSS2012-78 SS2012-78 |
The simplex method is one of the methods to derive rational assignments from linear constraints on ratiolals. It is know... [more] |
MSS2012-78 SS2012-78 pp.109-114 |
SS |
2013-01-10 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] |
SS2012-47 pp.7-12 |
SS |
2013-01-10 15:15 |
Okinawa |
|
Using SAT Solvers for Solving Control-Instruction Layout Problems in Low-Level 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] |
SS2012-50 pp.25-30 |
SS, IPSJ-SE |
2012-11-01 10:25 |
Hiroshima |
Hiroshima City University |
A SAT Encoding for Finding Operation Sequences of Malbolge that Implement Trit-wise Functions Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2012-37 |
Malbolge is known to be one of the most esoteric programming languages. Although it becomes possible to write programs i... [more] |
SS2012-37 pp.7-12 |
KBSE, SS |
2012-07-28 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.) SS2012-27 KBSE2012-29 |
[more] |
SS2012-27 KBSE2012-29 pp.103-108 |
SS |
2012-05-11 10:45 |
Ehime |
Ehime Univ. |
Introducing Array Mechanism into High-Level Assembly Language for Malbolge Satoshi Ando, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2012-8 |
Malbolge is known to be one of the most esoteric programming languages. Although it is possible to write programs in Mal... [more] |
SS2012-8 pp.43-48 |
SS, MSS |
2012-01-26 14:15 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
Automatic Generation of Non-linear Loop Invariants for Programs with Function Calls Eiichi Suzuki, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) MSS2011-61 SS2011-46 |
Finding loop invariants is one of the most important tasks in program verification. It is, however, difficult to automat... [more] |
MSS2011-61 SS2011-46 pp.39-44 |
SS, MSS |
2012-01-26 14:45 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
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.) MSS2011-62 SS2011-47 |
The word problem of an equation set is to decide, given two terms, whether the two terms are equivalent under the equati... [more] |
MSS2011-62 SS2011-47 pp.45-49 |
SS, MSS |
2012-01-26 15:30 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
On Rewriting Induction for Simply-typed Term Rewriting Systems Akira Ozeki, Keiichirou Kusakari, Tsubasa Sakata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) MSS2011-63 SS2011-48 |
Rewriting induction is a principle of proving inductive theorems by means of derivations obtained by applying inference ... [more] |
MSS2011-63 SS2011-48 pp.51-56 |
SS, MSS |
2012-01-26 16:00 |
Kochi |
Kochi City Culture-Plaza Cul-Port |
On Usable Rules under Argument Filterings in Higher-Order Rewrite Systems Kazuhiro Ooi, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) MSS2011-64 SS2011-49 |
The static dependency pair method is known as a powerful method for proving termination of higher-order rewrite systems ... [more] |
MSS2011-64 SS2011-49 pp.57-62 |
SS |
2011-10-28 12:15 |
Ishikawa |
JAIST |
Incorporating Elementary Symmetric Clauses into SAT Solvers with Two-Watched-Literal Scheme Yoshizane Hino, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2011-38 |
Umano et al.\ introduced elementary symmetric clauses (ES-clauses) into CNF formula in 2010 as a method for improving SA... [more] |
SS2011-38 pp.67-72 |
SS |
2011-03-07 14:45 |
Okinawa |
Okinawa-ken Seinen Kaikan |
Tree Automata with Constraints and their Closure-Properties Katsuhisa Kurahashi, Masahiko Sakai, Naoki Nishida, Futoshi Nomura, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2010-63 |
Tree automata are useful in analyzing properties of term rewriting systems since the class of recognizable tree language... [more] |
SS2010-63 pp.61-66 |
SS |
2010-12-14 16:20 |
Gunma |
Ikaho-Onsen Hotel Tenbo |
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, Toshiki Sakabe (Nagoya Univ.) SS2010-44 |
Detecting non-termination of term rewriting systems based on forward narrowing is used in termination tools such as APro... [more] |
SS2010-44 pp.31-36 |