3 papers
cs.LO2024
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System
Satoshi Kura, Hiroshi Unno
Verification of higher-order probabilistic programs is a challenging problem. We present a verification method that supports several quantitative properties of higher-order probabi…
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…