Showing cs.PLShow all
2 papers · 1 filter
cs.PL2022
Temporal Verification with Answer-Effect Modification
Taro Sekiyama, Hiroshi Unno
Type-and-effect systems are a widely-used approach to program verification, verifying the result of a computation using types, and the behavior using effects. This paper extends an…
cs.PL2016
Automating Induction for Solving Horn Clauses
Hiroshi Unno, Sho Torii
Verification problems of programs written in various paradigms (such as imperative, logic, concurrent, functional, and object-oriented ones) can be reduced to problems of solving H…