VLDB 2026 Research / reviewers in the wild / expert
Misaki Kojima
dblp:337/9297
· DBLP profile ↗
6ranked-venue papers
4as first author
6since 2021 · last 2026
0000-0001-5194-3947ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 5 · 3 first-author · 5 since 2021Theory of computation · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | Abstract Framework for All-Path Reachability Analysis toward Safety and Liveness VerificationabstractAn all-path reachability (APR, for short) predicate over an object set is a pair of a source set and a target set, which are subsets of the object set. APR predicates have been defined for abstract reduction systems (ARSs, for short) and then extended to logically constrained term rewrite systems (LCTRSs, for short) as pairs of constrained terms that represent sets of terms modeling configurations, states, etc. An APR predicate is partially (or demonically) valid w.r.t. a rewrite system if every finite maximal reduction sequence of the system starting from any element in the source set includes an element in the target set. Partial validity of APR predicates w.r.t. ARSs is defined by means of two inference rules, which can be considered a proof system to construct (possibly infinite) derivation trees for partial validity. On the other hand, a proof system for LCTRSs consists of four inference rules, leaving a gap between the inference rules for ARSs and LCTRSs. In this paper, we revisit the framework for APR analysis and adapt it to verification of not only safety but also liveness properties. To this end, we first reformulate an abstract framework for partial validity w.r.t. ARSs so that there is a one-to-one correspondence between the inference rules for partial validity w.r.t. ARSs and LCTRSs. Secondly, we show how to apply APR analysis to safety verification. Thirdly, to apply APR analysis to liveness verification, we introduce a novel stronger validity of APR predicates, called total validity, which requires not only finite but also infinite execution paths to reach target sets. Finally, for a partially valid APR predicate with a cyclic-proof tree, we show that the acyclicity of the proof graph obtained from the cyclic-proof tree is a necessary and sufficient condition for total validity. The condition implies that if there exists a cyclic-proof tree for an APR predicate, the proof graph of which is acyclic, then the APR predicate is totally valid. Misaki Kojima, Naoki Nishida 0001 |
FSCD | 1 |
| 2025 | Transforming concurrent programs with semaphores into logically constrained term rewrite systems
Misaki Kojima, Naoki Nishida 0001, Yutaka Matsubara |
J. Log. Algebraic Methods Program. | 1 |
| 2025 | Transforming imperative programs into bisimilar logically constrained term rewrite systems via injective functions from configurations to terms
Naoki Nishida 0001, Misaki Kojima, Takumi Kato |
J. Log. Algebraic Methods Program. | 2 |
| 2025 | A nesting-preserving transformation of SIMP programs into logically constrained term rewrite systems
Naoki Nishida 0001, Misaki Kojima, Ayuka Matsumi |
J. Log. Algebraic Methods Program. | 2 |
| 2023 | From Starvation Freedom to All-Path Reachability Problems in Constrained Rewriting
Misaki Kojima, Naoki Nishida 0001 |
PADL | 1 |
| 2023 | Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting
Misaki Kojima, Naoki Nishida 0001 |
J. Log. Algebraic Methods Program. | 1 |