21 citations · 101 across the 20 of their papers we have counts for
3 papers · 1 filter
On Integrating Deductive Synthesis and Verification Systems
Etienne Kneuss, Viktor Kuncak, Ivan Kuraj +1
We describe techniques for synthesis and verification of recursive functional programs over unbounded domains. Our techniques build on top of an algorithm for satisfiability modulo…
The Relationship between Craig Interpolation and Recursion-Free Horn Clauses
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
Despite decades of research, there are still a number of concepts commonly found in software programs that are considered challenging for verification: among others, such concepts…
Disjunctive Interpolants for Horn-Clause Verification (Extended Technical Report)
Philipp Rümmer, Hossein Hojjat, Viktor Kuncak
One of the main challenges in software verification is efficient and precise compositional analysis of programs with procedures and loops. Interpolation methods remain one of the m…