17 citations · 28 across the 18 of their papers we have counts for
4 papers · 1 filter
Interpolating Strong Induction
Hari Govind V K, Yakir Vizel, Vijay Ganesh +1
The principle of strong induction, also known as k-induction is one of the first techniques for unbounded SAT-based Model Checking (SMC). While elegant and simple to apply, propert…
Unification-based Pointer Analysis without Oversharing
Jakub Kuderski, Jorge A. Navas, Arie Gurfinkel
Pointer analysis is indispensable for effectively verifying heap-manipulating programs. Even though it has been studied extensively, there are no publicly available pointer analyse…
Property Directed Self Composition
Ron Shemer, Arie Gurfinkel, Sharon Shoham +1
We address the problem of verifying k-safety properties: properties that refer to k-interacting executions of a program. A prominent way to verify k-safety properties is by self co…
Local Reasoning for Parameterized First Order Protocols
Rylo Ashmore, Arie Gurfinkel, Richard Trefler
First Order Logic (FOL) is a powerful reasoning tool for program verification. Recent work on Ivy shows that FOL is well suited for verification of parameterized distributed system…