Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
SS |
2023-03-15 09:30 |
Okinawa |
(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 |
IN, NS (Joint) |
2023-03-03 11:40 |
Okinawa |
Okinawa Convention Centre + Online (Primary: On-site, Secondary: Online) |
A Design and Implementation of Unit Test Tool for Client-Side Web Programming Learning Assistant System Inzali Naing, Nobuo Funabiki, Khaing Hsu Wai (Okayama Univ.), Htoo Htoo Sandi Kyaw (TUAT), Huiyu Qi, Veronicha Flasma (Okayama Univ.) NS2022-235 |
[more] |
NS2022-235 pp.390-395 |
SS |
2020-03-04 15:10 |
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 |
MSS, SS |
2019-01-16 09:25 |
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 |
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 |
ET |
2014-07-05 15:00 |
Akita |
Akita Univ. |
Learning by Reading Computer Programs: Design of a Support System Takahito Tomoto, Takako Akakura (TUS) ET2014-26 |
Learning about programming requires the development of two different skills: learning the program syntax necessary to wr... [more] |
ET2014-26 pp.23-26 |
SS, KBSE |
2013-07-26 09:30 |
Hokkaido |
|
Conditional Dependency Pair Method for Proving Termination of Functional Programs with Exception Handling Takeshi Hamaguchi, Masahiko Sakai (Nagoya Univ.) SS2013-23 KBSE2013-23 |
We have recently proposed a method for proving termination/non-termination properties of eager-evaluation-based function... [more] |
SS2013-23 KBSE2013-23 pp.61-66 |
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 |
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 |
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 |
SP, WIT |
2008-05-29 - 2008-05-30 |
Hyogo |
Kobe University |
Development of the training support software for writing motions Kanako Yoshino, Masami Takata (Nara Women's Univ.), Seiichi Tenpaku (Arcadia), Kazuki Joe (Nara Women's Univ.) SP2008-14 WIT2008-14 |
We develope a training system of hand-write training for children with difficulty of writing motions. The typical traini... [more] |
SP2008-14 WIT2008-14 pp.79-84 |
SS |
2008-03-03 13:05 |
Nagasaki |
Nagasaki Univ. |
Static Dependency Pair Method for Simply-Typed Term Rewriting and Related Techniques Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) SS2007-61 |
We proposed a static dependency pair method,
which can effectively prove termination of functional programs.
Since the... [more] |
SS2007-61 pp.25-30 |
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 |
SS, KBSE |
2006-10-26 16:15 |
Ehime |
Ehime University |
Example programs generated by GeneSys and proposal of Introduction rule Satoru Kondo, Masahiko Sakai, Naoki Nishida, Toshiki Sakabe, Keiichirou Kusakari (Nagoya Univ.) |
Program Generation System GeneSys is a method for generating executable programs from specifications described in first-... [more] |
SS2006-46 KBSE2006-22 pp.37-42 |
SS |
2005-12-20 10:15 |
Kochi |
Kochi Women's University |
Enhancing Dependency Pair Method by Strong Computability in Simply-Typed Term Rewriting Systems Keiichirou Kusakari, Masahiko Sakai (Nagoya Univ.) |
We enhance the dependency pair method to prove termination by recursive structure analysis in the simply-typed term rewr... [more] |
SS2005-65 pp.13-18 |
SS |
2005-06-24 10:45 |
Nagano |
Shinshu Univ. Ohta-Kokusai-Kinenkan |
On Proving Termination of Simply-Typed Term Rewriting Systems Based on Strong Computability Keiichirou Kusakari, Takahiro Sakurai, Naoki Nishida, Masahiko Sakai, Toshiki Sakabe (Nagoya Univ.) |
Terminating functional programs are safe in execution, and valuable because their reduction relations are suitable for i... [more] |
SS2005-21 pp.19-24 |
SS |
2005-06-24 11:45 |
Nagano |
Shinshu Univ. Ohta-Kokusai-Kinenkan |
Dependency Graph Method for Proving Termination of Narrowing Koichi Miura, Naoki Nishida, Masahiko Sakai, Keiichirou Kusakari, Toshiki Sakabe (Nagoya Univ.) |
Term rewriting systems with extra variables (called EV-TRSs) has an ability to represent inverse-computation programs, a... [more] |
SS2005-23 pp.31-36 |