Avy

Interpolating Property Directed Reachablility

About

Avy is an AIGER Model Checker that combines Interpolation and Property Directed Rachability developed by Arie Gurfinkel and Yakir Vizel.

Benchmark	solved	sat	unsat
hwmcc12 (details)	125	31	94
hwmcc13 (details)	107	27	80
hwmcc14cav (details)	103	33	70

Arie Gurfinkel and Yakir Vizel. Interpolating Property Directed Reachability. CAV 2014. (PDF) (Video)
Arie Gurfinkel and Yakir Vizel. DRUPing for Interpolants. FMCAD 2014. (PDF) (Plots)
Yakir Vizel, Arie Gurfinkel, and Sharad Malik. Fast Interpolating BMC. CAV 2015. (PDF)
Hari Govind V K, Yakir Vizel, Arie Gurfinkel, and Vijay Ganesh. Interpolating Stong Induction. CAV 2019. (PDF) (Plots) (Results)