Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
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 |
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 |
SS |
2009-12-17 16:20 |
Kagawa |
Kagawa Univ. |
On Decidability of Context-Sensitive Termination for Right-Linear Right-Shallow Term Rewriting Systems Yoshimasa Mishuku, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2009-40 |
It is known that termination and innermost termination are decidable for term rewriting systems (TRSs for short) whose d... [more] |
SS2009-40 pp.31-36 |
SS |
2009-12-18 08:40 |
Kagawa |
Kagawa Univ. |
Program Generation Based on Transformation of Conditional Equations Masanori Nagashima, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida, Keiichirou Kusakari (Nagoya Univ.) SS2009-41 |
Program-generation system GeneSys, which we have ever proposed, generates executable programs from first order equationa... [more] |
SS2009-41 pp.37-42 |
SS |
2008-12-19 10:00 |
Kochi |
Kochi Univiersity of Technology |
Solving Satisfiability of CNF Formulas with Elementary Symmetric Functions Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2008-44 |
In recent years, several efficient SAT solvers, which decide satisfiability of boolean formulas, have been developed.
S... [more] |
SS2008-44 pp.31-36 |
SS |
2008-12-19 10:30 |
Kochi |
Kochi Univiersity of Technology |
Decidability of Termination Properties for Term Rewriting Systems Consisting of Shallow Dependency Pairs Keita Uchiyama, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2008-45 |
In this paper, we show some decidable properties: termination, innermost termination and context-sensitive termination f... [more] |
SS2008-45 pp.37-42 |
SS |
2008-10-17 11:00 |
Yamanashi |
University of Yamanashi, Kofu Campus |
Behavior Analysis of Scalable CAN Protocol on a Bit-Error Channel Kenji Ukai, Toshiki Sakabe, Hiroaki Takada, Ryo Kurachi, Masahiko Sakai, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2008-37 |
Scalable CAN protocol is an improvement of the original CAN (Controller Area Network) protocol so that more than ten tim... [more] |
SS2008-37 pp.61-66 |
SS |
2008-07-31 17:30 |
Hokkaido |
Future University-Hakodate |
A Reduction Order for Orienting Equations in Theorem Proving of Constrained TRSs Naoki Nishida, Tsubasa Sakata, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) SS2008-20 |
In automated theorem proving, we often face cases where the procedure
keeps running. To avoid such cases, the theorem p... [more] |
SS2008-20 pp.43-48 |
KBSE, SS |
2008-05-29 13:30 |
Miyazaki |
Miyazaki Citizens' Plaza |
On Rewriting Induction for Presburger-Constrained Term Rewriting Systems Tsubasa Sakata, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari (Nagoya Univ.) SS2008-1 KBSE2008-1 |
A method for verifying equivalence between procedural programs has been proposed, where the implicit induction is extend... [more] |
SS2008-1 KBSE2008-1 pp.1-6 |
SS |
2008-03-03 11:00 |
Nagasaki |
Nagasaki Univ. |
Error Detection with Soft Typing for Dynamically Typed Languages Akihisa Yamada, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) SS2007-59 |
We propose a rich extension of soft typing for dynamically-typed languages like LISP,
and prove its soundness.
This e... [more] |
SS2007-59 pp.13-18 |
SS |
2008-03-03 13:30 |
Nagasaki |
Nagasaki Univ. |
A Sufficient Condition for Termination of Transformations from Equations to Rewrite Rules Kiyotaka Mizuno, Naoki Nishida, Toshiki Sakabe, Masahiko Sakai, Keiichirou Kusakari (Nagoya Univ.) SS2007-62 |
Several procedures which transform pairs of term rewriting systems (TRSs, for short) and sets of equations into equivale... [more] |
SS2007-62 pp.31-36 |
SS |
2007-12-17 14:00 |
Shimane |
Shimane Univ. |
Extending program-generation system GeneSys for allowing negation in equational specifications Satoru Kondo, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari, Naoki Nishida (Nagoya Univ.) SS2007-45 |
[more] |
SS2007-45 pp.43-48 |
SS |
2007-12-17 17:00 |
Shimane |
Shimane Univ. |
A tool for designing Sudoku problems by interactive fill-in approach Yohei Umano, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Uni.) SS2007-50 |
In recent years, efficient SAT solvers, which decide satisfiability of boolean formulae, have been developed and used in... [more] |
SS2007-50 pp.73-78 |
SS |
2007-10-22 14:00 |
Miyagi |
Miyagi Univ. |
Proving Non-termination of Logic Programs by Detecting Loops in Derivation Trees Tomohiro Mizutani, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2007-30 |
In this paper, we present a method for automatically proving non-termination of logic programs. Given a program and a qu... [more] |
SS2007-30 pp.1-6 |
SS |
2007-08-02 13:30 |
Hokkaido |
Hokkaido Univ. |
Recognizable Approximation of Descendant Sets for Left-Linear Oriented Conditional Term Rewriting Systems Toshiki Murata, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2007-16 |
The reachability problem for term rewriting systems (TRSs) is to decide whether one of two given terms is reachable to t... [more] |
SS2007-16 pp.1-6 |
SS |
2007-08-02 14:00 |
Hokkaido |
Hokkaido Univ. |
Implicit Induction for Proving Behavioral Equivalence by Equational Rewriting Yuji Sasada, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) SS2007-17 |
A behavioral specification is a description of what is supposed to happen.
Two states are said to be behaviourally equi... [more] |
SS2007-17 pp.7-12 |
SS |
2007-06-22 09:30 |
Ishikawa |
JAIST |
Static Dependeycy Pair Method for Proving Termination of Higher-Order Rewriting Systems Keiichirou Kusakari, Yasuo Isogai, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) SS2007-12 |
A higher-order rewriting systems (HRS) is a computational model that provides operational semantics for functional progr... [more] |
SS2007-12 pp.17-22 |
SS |
2007-06-22 10:10 |
Ishikawa |
JAIST |
Argument Filtering Method on Second-Order Rewriting System Yasuo Isogai, Keiichirou Kusakari, Masahiko Sakai, Toshiki Sakabe, Naoki Nishida (Nagoya Univ.) SS2007-13 |
Higher-order rewrite systems are computation models of functional programming languages, and the termination property is... [more] |
SS2007-13 pp.23-28 |
SS |
2006-12-14 13:40 |
Fukuoka |
Kyushu University |
Automated Theorem Prover HOPSYS on Simply-Typed Rewriting Systems Akinori Kamada, Keiichirou Kusakari, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ) |
[more] |
SS2006-57 pp.7-12 |
SS, KBSE |
2006-10-26 13:40 |
Ehime |
Ehime University |
Approach to Software Verification Based on Transforming from Procedural Programs to Rewrite Systems Yuki Furuichi, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
In the field of term rewriting, inductionless induction and rewriting
induction have been widely studied as methods for... [more] |
SS2006-41 KBSE2006-17 pp.7-12 |