Committee |
Date Time |
Place |
Paper Title / Authors |
Abstract |
Paper # |
MSS, SS |
2023-01-11 13:30 |
Osaka |
(Osaka, Online) (Primary: On-site, Secondary: Online) |
A formal description of a functional language with exception handling, and constrained dependency pairs for the termination proofs Takeshi Hamaguchi, Masahiko Sakai (Nagoya Univ.) MSS2022-56 SS2022-41 |
This paper proposes a termination-proof method for functional programs with exception handling. First, we give a small s... [more] |
MSS2022-56 SS2022-41 pp.66-71 |
SS, MSS |
2022-01-12 09:40 |
Nagasaki |
Nagasakiken-Kensetsu-Sogo-Kaikan Bldg. (Nagasaki, Online) (Primary: On-site, Secondary: Online) |
On Constrained Rewrite Rules Representing Semantics Rules of LLVM IR Takumi Kato, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2021-47 SS2021-34 |
A method to verify programs written in a simple C-like language via logically constrained term rewrite systems (LCTRS, f... [more] |
MSS2021-47 SS2021-34 pp.89-94 |
MSS, SS |
2021-01-27 15:00 |
Online |
Online (Online) |
Speeding up combinatorial optimization solver CombSQL+ by introducing Pseudo-Boolean constraints Junichiro Kishi, Masahiko Sakai, Naoki Nishida, Kenji Hashimoto (Nagoya univ.) MSS2020-40 SS2020-25 |
The authors have proposed a solver CombSQL+ for combinatorial optimization problems (COPs) described in extended SQL lan... [more] |
MSS2020-40 SS2020-25 pp.66-71 |
SS |
2020-03-04 13:50 |
Okinawa |
(Okinawa) (Cancelled but technical report was issued) |
A Decision Procedure for a Macro Forest Transducer being an Implementation of an XML Schema Mapping Hiroaki Tabata, Masahiko Sakai, Kenji Hashimoto (Nagoya Univ. G. S.) SS2019-43 |
XML Schema Mapping (SM) describes the correspondence between two different XML Schema DTDs using a tree pattern.
A dete... [more] |
SS2019-43 pp.13-18 |
SS |
2020-03-04 15:10 |
Okinawa |
(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 |
DC, SS |
2019-10-24 14:55 |
Kumamoto |
Kumamoto Univ. (Kumamoto) |
Extending rewriting induction to existentially quantified equations Kazushi Nishie, Naoki Nishida, Masahiko sakai (Nagoya Univ.) SS2019-17 DC2019-45 |
In this paper, we extend rewriting induction which is developed to prove equations, to existentially quantified equation... [more] |
SS2019-17 DC2019-45 pp.25-30 |
SS |
2019-03-04 16:45 |
Okinawa |
(Okinawa) |
SQL queries for generating input constraints of SMT solvers from descriptions of combinatorial optimization problems Genki Sakanashi, Masahiko Sakai, Naoki Nishida, Kenji Hashimoto (Nagoya Univ.) SS2018-66 |
The authors recently proposed an SQL-based language CombSQL+ for specifying combinatorial optimization problems, and sho... [more] |
SS2018-66 pp.85-90 |
MSS, SS |
2019-01-16 09:25 |
Okinawa |
(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 |
2019-01-16 09:50 |
Okinawa |
(Okinawa) |
Extending Narrowing Trees to Basic Narrowing in Term Rewriting Yuya Maeda, Naoki Nishida, Masahiko Sakai, Tomoya Kobayashi (Nagoya Univ.) MSS2018-68 SS2018-39 |
Narrowing computation of a term rewriting system is an extension of rewriting by replacing matching with unification, wh... [more] |
MSS2018-68 SS2018-39 pp.73-78 |
SS, KBSE, IPSJ-SE [detail] |
2017-07-20 15:50 |
Hokkaido |
(Hokkaido) |
Polynomial Interpretations to Convert Dependency Chains of Constrained Term Rewriting Systems to Bounded Increasing Sequences of Intergers Tomohiro Sasano, Naoki Nishida, Masahiko Sakai, Tomoya Ueyama (Nagoya Univ.) SS2017-17 KBSE2017-17 |
In dependency pair framework for proving termination of constrained term rewriting systems, polynomial interpretations t... [more] |
SS2017-17 KBSE2017-17 pp.139-144 |
SS, KBSE, IPSJ-SE [detail] |
2017-07-20 16:15 |
Hokkaido |
(Hokkaido) |
A compiler that translates to Malbolge from a C-language subset containing recursive calls Genki Sakanashi, Shohei Kobe, Masahiko Sakai, Naoki Nishida, Kenji Hashimoto (Nagoya Univ.) SS2017-18 KBSE2017-18 |
Malbolge is an esoteric programming language, which is promising to protect intellectual property rights due to its diff... [more] |
SS2017-18 KBSE2017-18 pp.145-150 |
SS |
2017-03-09 09:55 |
Okinawa |
(Okinawa) |
Logical Formula Simplification and Static Analysis for Quantitative Information Flow Analysis using Model Counting Masato Nakashima, Kenji Hashimoto, Masahiko Sakai, Hiroyuki Seki (Nagoya Univ.) SS2016-61 |
Model counting is one of the promising methods for quantitative information flow analysis. In this paper, we focus on th... [more] |
SS2016-61 pp.7-12 |
DC, SS |
2016-10-27 15:30 |
Shiga |
Hikone Kinro-Fukushi Kaikan Bldg. (Shiga) |
Efficiency Improvement in #SMT-based Quantitative Information Flow Analysis Masato Nakashima, Trung Chu Bao, Kenji Hashimoto, Masahiko Sakai, Hiroyuki Seki (Nagoya Univ.) SS2016-26 DC2016-28 |
Model counting is one of the promising methods for quantitative information flow analysis. In this paper, we focus on th... [more] |
SS2016-26 DC2016-28 pp.49-54 |
KBSE, SS, IPSJ-SE [detail] |
2016-07-14 13:40 |
Hokkaido |
(Hokkaido) |
An intermediate language for a compiler generating highly obfuscated Malbolge codes Shohei Kobe, Masahiko Sakai, Naoki Nishida, Hiroyuki Seki (Nagoya Univ.) SS2016-12 KBSE2016-18 |
[more] |
SS2016-12 KBSE2016-18 pp.105-110 |
SS |
2016-03-10 10:50 |
Okinawa |
(Okinawa) |
An extension of SQL for specifying combinatorial optimization problems Yusaku Uchida, Masahiko Sakai, Naoki Nishida (Nagoya Univ.) SS2015-80 |
The performance of satisfiability (SAT) solvers have incredibly improved in recent years.
It is, however, difficult to ... [more] |
SS2015-80 pp.25-30 |
SS |
2016-03-10 11:15 |
Okinawa |
(Okinawa) |
Program Verification Using Non-linear Loop Invariants Generated by Partially Applying an Extended Farkas' Lemma Makishi Yanagisawa, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) SS2015-81 |
To generate loop invariants, methods that, using Farkas' lemma, convert verification formulas obtained from a given temp... [more] |
SS2015-81 pp.31-36 |
SS, MSS |
2016-01-25 16:45 |
Ishikawa |
Shiinoki-Geihin-Kan (Ishikawa) |
On Proving Termination and Inductive Theorems Simultaneously for Constrained Term Rewriting Systems Yoshifumi Kawamoto, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2015-48 SS2015-57 |
[more] |
MSS2015-48 SS2015-57 pp.75-80 |
SS, MSS |
2016-01-25 17:10 |
Ishikawa |
Shiinoki-Geihin-Kan (Ishikawa) |
A method for making proof graph finite on disjunctive parameterised Boolean equation systems Yutaro Nagae, Masahiko Sakai, Hiroyuki Seki (Nagoya Univ.) MSS2015-49 SS2015-58 |
A parameterised Boolean equation system (PBES) is a set of equations that defines sets as the least and/or greatest fixe... [more] |
MSS2015-49 SS2015-58 pp.81-85 |
SS, MSS |
2016-01-26 11:05 |
Ishikawa |
Shiinoki-Geihin-Kan (Ishikawa) |
Transforming Constrained Dependency Pairs by Narrowing Tomohiro Sasano, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) MSS2015-57 SS2015-66 |
The dependency pair framework, a method for proving termination of term rewriting systems, has been extended for constra... [more] |
MSS2015-57 SS2015-66 pp.123-128 |
KBSE, SS, IPSJ-SE [detail] |
2015-07-24 11:10 |
Hokkaido |
(Hokkaido) |
An Equivalent Transformation of Constrained Term Rewriting Systems by Pattern Elimination Takahiro Nagao, Naoki Nishida, Masahiko Sakai (Nagoya Univ.) SS2015-33 KBSE2015-26 |
A constrained term rewriting system, an extension of term rewriting systems, can control application of rules by constra... [more] |
SS2015-33 KBSE2015-26 pp.167-172 |