6 citations · 6 across the 4 of their papers we have counts for
5 papers · 1 filter
A Primal-Dual Perspective on Program Verification Algorithms (Extended Version)
Takeshi Tsukada, Hiroshi Unno, Oded Padon +1
Many algorithms in verification and automated reasoning leverage some form of duality between proofs and refutations or counterexamples. In most cases, duality is only used as an i…
Constraint-based Relational Verification
Hiroshi Unno, Tachio Terauchi, Eric Koskinen
In recent years they have been numerous works that aim to automate relational verification. Meanwhile, although Constrained Horn Clauses (CHCs) empower a wide range of verification…
Toward Neural-Network-Guided Program Synthesis and Verification
Naoki Kobayashi, Taro Sekiyama, Issei Sato +1
We propose a novel framework of program and invariant synthesis called neural network-guided synthesis. We first show that, by suitably designing and training neural networks, we c…
Program Verification via Predicate Constraint Satisfiability Modulo Theories
Hiroshi Unno, Yuki Satake, Tachio Terauchi +1
This paper presents a verification framework based on a new class of predicate Constraint Satisfaction Problems called pCSP where constraints are represented as clauses modulo firs…
Refinement Type Inference via Horn Constraint Optimization
Kodai Hashimoto, Hiroshi Unno
We propose a novel method for inferring refinement types of higher-order functional programs. The main advantage of the proposed method is that it can infer maximally preferred (i.…