6 citations · 9 across the 14 of their papers we have counts for
5 papers · 1 filter
Software Model-Checking as Cyclic-Proof Search
Takeshi Tsukada, Hiroshi Unno
This paper shows that a variety of software model-checking algorithms can be seen as proof-search strategies for a non-standard proof system, known as a cyclic proof system. Our us…
Learning Heuristics for Template-based CEGIS of Loop Invariants with Reinforcement Learning
Minchao Wu, Takeshi Tsukada, Hiroshi Unno +2
Loop-invariant synthesis is the basis of program verification. Due to the undecidability of the problem in general, a tool for invariant synthesis necessarily uses heuristics. Desp…
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…
Decision Tree Learning in CEGIS-Based Termination Analysis
Satoshi Kura, Hiroshi Unno, Ichiro Hasuo
We present a novel decision tree-based synthesis algorithm of ranking functions for verifying program termination. Our algorithm is integrated into the workflow of CounterExample G…
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…