Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
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 |
2012-05-11 11:15 |
Ehime |
Ehime Univ. |
Static Dependecy Pair Method in Rewriting Systems for Functional Programs with Product, Algebraic Data, and ML-Polymorphic Types Keiichirou Kusakari (Nagoya Univ.) SS2012-9 |
For simply-typed term rewriting systems (STRSs)
and higher-order rewrite systems (HRSs) {\em \`a la} Nipkow,
we propo... [more] |
SS2012-9 pp.49-54 |
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 |
SS |
2010-10-15 11:00 |
Iwate |
Iwate Prefectural Univ. |
On DPLL Transition Systems Modulo Equational Theories Tatsuya Baba, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) SS2010-36 |
SMT solvers are tools for deciding satisfiability of formulas under given theories such as arrays, lists, queues and so ... [more] |
SS2010-36 pp.49-54 |
SS |
2010-10-15 11:30 |
Iwate |
Iwate Prefectural Univ. |
On Turing Completness of an Esoteric Language, Malbolge Satoshi Nagasaka, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2010-37 |
Malbolge is known as one of the most esoteric programming languages. In this paper, we prove that Malbolge is weakly Tur... [more] |
SS2010-37 pp.55-60 |
SS |
2010-08-05 16:00 |
Hokkaido |
Asahikawa Shimin-Bunka-Kaikan (Civic Culture Hall) |
Argument Filterings and Usable Rules in Higher-Order Rewrite Systems Sho Suzuki, Keiichirou Kusakari (Nagoya Univ.), Frederic Blanqui (INRIA) SS2010-24 |
The static dependency pair method is a method for proving the termination
of higher-order rewrite systems {\em \`a la} ... [more] |
SS2010-24 pp.47-52 |
SS |
2009-12-17 15:50 |
Kagawa |
Kagawa Univ. |
Argument Filtering and Usable Rules in Higher-Order Rewrite Systems Sho Suzuki, Keiichirou Kusakari, Toshiki Sakabe, Masahiko Sakai, Naoki Nishida (Nagoya Univ.) SS2009-39 |
Simply-typed term rewriting systems (STRSs) and higher-order rewrite systems (HRSs)
have been proposed to extend term r... [more] |
SS2009-39 pp.25-30 |