Verification Series

Efficient Implementation of Property Directed Reachability

30th November 2017, 14:00 add to calender
Boris Konev

Abstract

’d like to discuss the IC3 (AKA Property Directed Reachability) method, which has been praised as the biggest advance in hardware model checking of modern time.
I wanted to look into how this method works and how it compares with temporal resolution for a while now, so this seems to be a perfect opportunity.

Specifically, I will give an overview of Niklas Even, Anal Mishchenko, Robert Brayton “Efficient Implementation of Property Directed Reachability”, FMCAD 2011 but might also look into other papers.
add to calender (including abstract)