16 citations · 20 across the 8 of their papers we have counts for
8 papers
The 19th International Workshop on Termination (WST 2023): Preface, Invited Talk Abstract, and Tool Descriptions
Akihisa Yamada, Benjamin Lucien Kaminski, Dieter Hofbauer +2
This report contains the proceedings of the 19th International Workshop on Termination (WST 2023), which was held in Obergurgl during August 24--25 as part of Obergurgl Summer on R…
Goal-Aware RSS for Complex Scenarios via Program Logic
Ichiro Hasuo, Clovis Eberhart, James Haydon +12
We introduce a goal-aware extension of responsibility-sensitive safety (RSS), a recent methodology for rule-based safety guarantee for automated driving systems (ADS). Making RSS r…
Fixed Points Theorems for Non-Transitive Relations
Jérémy Dubut, Akihisa Yamada
In this paper, we develop an Isabelle/HOL library of order-theoretic fixed-point theorems. We keep our formalization as general as possible: we reprove several well-known results a…
Relational Differential Dynamic Logic
Juraj Kolčák, Ichiro Hasuo, Jérémy Dubut +3
In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely re…
On Probabilistic Term Rewriting
Martin Avanzini, Ugo Dal Lago, Akihisa Yamada
We study the termination problem for probabilistic term rewrite systems. We prove that the interpretation method is sound and complete for a strengthening of positive almost sure t…
Nagoya Termination Tool
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
This paper describes the implementation and techniques of the Nagoya Termination Tool, a termination prover for term rewrite systems. The main features of the tool are: the first i…
A Unified Ordering for Termination Proving
Akihisa Yamada, Keiichirou Kusakari, Toshiki Sakabe
We introduce a reduction order called the weighted path order (WPO) that subsumes many existing reduction orders. WPO compares weights of terms as in the Knuth-Bendix order (KBO),…
AC-KBO Revisited
Akihisa Yamada, Sarah Winkler, Nao Hirokawa +1
Equational theories that contain axioms expressing associativity and commutativity (AC) of certain operators are ubiquitous. Theorem proving methods in such theories rely on well-f…