記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

A logically constrained term rewrite system (LCTRS, for short) modeling a concurrent program is usually non-terminating, left-linear, and overlapping, but sometimes confluent w.r.t. an initial ground term which corresponds to an initial configuration of the program. In this paper, we show how to prove confluence of such an LCTRS w.r.t. the initial term. To be more precise, we add the rule from the initial term to a fresh constant to the LCTRS, and construct a proof tree for the all-path reachability problem from the initial term to the constant. If the directed graph obtained from the proof tree by considering it as a cyclic proof is strongly connected and each node corresponds to a single term, then all terms reachable from the initial term can be reduced back to the initial one and thus the original LCTRS is confluent w.r.t. the initial one.

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）   出版者・発行元：Information Processing Society of Japan  

An all-path reachability (APR, for short) problem of a logically constrained term rewrite system (LCTRS, for short) is a pair of constrained terms representing state sets. An APR problem is demonically valid if every finite execution path from any state in the first set to an irreducible state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by an LCTRS to an APR problem with irreducible constant destinations. In this paper, by focusing on quasi-termination of constrained narrowing, we characterize a class of LCTRSs of which APR problems with constant destinations are decidable. Quasi-termination of a (constrained) term w.r.t. narrowing is the finiteness of the set of reachable narrowed (constrained) terms from the initial (constrained) term up to variable renaming (and equivalence of constraints). To this end, we first introduce an inference rule for disproofs to a proof system for APR problems with constant destinations and formulate (dis)proof trees of APR problems in the style of cyclic proofs. Secondly, to prove correctness of disproof trees, we adapt constrained narrowing to LCTRSs and show soundness of constrained narrowing of LCTRSs w.r.t. constrained rewriting. Thirdly, we show a sufficient condition of LCTRSs for quasi-termination of constrained narrowing starting from linear constrained terms that have no nesting of defined symbols: Rewrite rules are right-linear and nesting-free w.r.t. defined symbols, and the application of rewrite rules for (mutually) recursive defined symbols does not increase the height of resulting constrained terms of narrowing. Finally, we show that if a constrained term is quasi-terminating w.r.t. narrowing of an LCTRS over a sort-wise finite signature with a decidable theory, then the APR problem consisting of the constrained term and an irreducible constant is decidable.

DOI： 10.2197/ipsjjip.32.417

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（学術雑誌）  

A concurrent program with semaphore-based exclusive control can be modeled by a logically constrained term rewrite system. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem of the system is a pair of state sets and is demonically valid if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, we propose a weakened but easily-implementable variant of an existing proof system for all-path reachability problems. As a case study, we deal with the race freedom of concurrent programs with semaphore-based exclusive control.

DOI： 10.1016/j.jlamp.2023.100903

Open Access

記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

As for term rewrite systems, the dependency pair (DP, for short) framework with several kinds of DP processors is useful for proving termination of logically constrained term rewrite systems (LCTRSs, for short). However, the polynomial interpretation processor is not so effective against LCTRSs with bit-vector arithmetic (BV-LCTRSs, for short). In this paper, we propose a novel DP processor for BV-LCTRSs to solve a singleton DP problem consisting of a dependency pair forming a self-loop. The processor is based on an acyclic directed graph such that the nodes are bit-vectors and any dependency chain of the problem is projected to a path of the graph. We show a sufficient condition for the existence of such an acyclic graph, and simplify it for a specific case.

DOI： 10.48550/arXiv.2307.14094

記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

In the last decade, several transformations of an imperative program into a logically constrained term rewrite system (LCTRS, for short) have been investigated and extended. They do not preserve the nesting of statements, generating rewrite rules like transition systems, while function calls are represented by the nesting of function symbols. Structural features of the original program must be often useful in analyzing the transformed LCTRS, but, to use such features, we have to know how to transform the program into the LCTRS, e.g., we keep the correspondence between statements in the program and the introduced auxiliary function symbols in the LCTRS. In this paper, we propose a nesting-preserving transformation of a SIMP program (a C integer program) into an LCTRS. The transformation is almost based on previous work and introduces the nesting of function symbols that correspond to statements in the original program. To be more precise, we propose a construction of a tree homomorphism which is used as a post-process of the transformation in previous work, i.e., which is applied to the LCTRS obtained from the program. As a correctness of the nesting-preserving transformation, we show that the tree homomorphism is sound and complete for the reduction of the LCTRS.

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

A transformation of concurrent programs with semaphore-based exclusive control and waiting queues into logically constrained term rewrite systems (LCTRSs, for short) has been proposed. To represent waiting queues, the transformation adopts a turn waiting system with number tickets, while the use of usual lists is a straightforward approach. In this abstract, we show a list-based approach to waiting queues and compare the two approaches by means of verification of race freedom of a simple reader-writer example.

記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

ビットベクトル制約付き項書換え系（BV-LCTRS）はC言語などのプログラムのモデルとして有用である．等価性検証に書換え帰納法を用いる際には，与えられた書換え系に帰納法の仮定となる書換え規則を加えて得られる書換え系の停止性が何度も証明される. LCTRSの停止性証明には項書換え系と同様に依存対プロセッサを使用して証明する枠組みの依存対フレームワークが用いられるが，整数制約を持つLCTRSの停止性証明において最も強力なプロセッサの1つである多項式解釈プロセッサはBV-LCTRSには適用できない．本稿では，BV-LCTRSの停止性証明を強化することを目的として，新たな依存対プロセッサとしてビットベクトル上の多項式解釈プロセッサと単一自己ループ除去プロセッサを提案する．

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）   出版者・発行元：Springer, Cham  

An all-path reachability problem of a logically constrained term rewrite system is a pair of constrained terms representing state sets, and is demonically valid if every finite execution path from any state in the first set to a terminating state includes a state in the second set. We have proposed a framework to reduce the non-occurrence of specified error states in a transition system represented by a logically constrained term rewrite system to an all-path reachability problem of the system. In this paper, we extend the framework to verification of starvation freedom of asynchronous integer transition systems with shared variables such that some processes enter critical sections.

DOI： 10.1007/978-3-031-24841-2_11

記述言語：英語   掲載種別：研究論文（研究会，シンポジウム資料等）  

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

A concurrent program with semaphore-based exclusive control can be transformed into a logically constrained term rewrite system that is computationally equivalent to the program. In this paper, we first propose a framework to reduce the non-occurrence of a specified runtime error in the program to an all-path reachability problem of the transformed logically constrained term rewrite system. Here, an all-path reachability problem is a pair of state sets and is true if every finite execution path starting with a state in the first set and ending with a terminating state includes a state in the second set. Then, as a case study, we show how to apply the framework to the race-freeness of semaphore-based exclusive control in the program. Finally, we show a simplified variant of a proof system for all-path reachability problems.

記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

To transform an imperative program into a logically constrained term rewrite system (LCTRS, for short), previous work converts a statement list to rewrite rules in a stepwise manner, and proves the correctness along such a conversion and the big-step semantics of the program. On the other hand, the small-step semantics of a programming language comprises of inference rules that define transition steps of configurations. Partial instances of such inference rules are almost the same as rewrite rules in the transformed LCTRS. In this paper, we aim at establishing a framework for plain definitions and correctness proofs of transformations from programs into LCTRSs. To this end, for the transformation in previous work, we show an injective function from configurations to terms, and reformulate the transformation by means of the injective function. The injective function maps a transition step to a reduction step, and results in a plain correctness proof.

担当区分：筆頭著者   記述言語：日本語   掲載種別：研究論文（研究会，シンポジウム資料等）  

担当区分：筆頭著者   記述言語：英語   掲載種別：研究論文（国際会議プロシーディングス）  

担当区分：筆頭著者   記述言語：日本語  

計算モデルである論理制約付き項書換え系（LCTRS）をプログラムの検証に用いる先行研究では，逐次実行される命令型プログラムを対象としている．現実の計算機の利用状況を考えると，逐次実行されるプログラムとそれを並行化したプログラムが等価であることを検証したいという要求がある．本稿では，並行実行されるプログラムをLCTRSで表現すること目的として，セマフォによる排他制御を含むプログラムをLCTRSで表現する方法を提案する．そのためにまず，先行研究で導入された実行環境を表す関数記号の引数を，実行されるプロセスの数だけ増やすことで，プロセスの並行実行を表現する．次に，セマフォに対する操作を書換え規則で表現し，セマフォによる排他制御を含むプログラムをLCTRSに変換する．セマフォに対する待ち行列を番号札を使って管理することで，リストなどの再帰データ構造を導入せずにセマフォの操作を表現する．