3 papers
cs.LO2026
Truth Predicate of Inductive Definitions and Logical Complexity of Infinite-Descent Proofs
Sohei Ito, Makoto Tatsuta
Formal reasoning about inductively defined relations and structures is widely recognized not only for its mathematical interest but also for its importance in computer science, and…
cs.LO2025
Encoding Peano Arithmetic in a Minimal Fragment of Separation Logic
Sohei Ito, Makoto Tatsuta
Separation logic is successful for software verification of heap-manipulating programs. Numbers are necessary to be added to separation logic for verification of practical software…
cs.PL2018
Semantical Equivalence of the Control Flow Graph and the Program Dependence Graph
Sohei Ito
The program dependence graph (PDG) represents data and control dependence between statements in a program. This paper presents an operational semantics of program dependence graphs…