Efficient Implementation of Property Directed Reachability

30^th November 2017, 14:00
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.