FMCAD 2004 START ConferenceManager    

Simple yet efficient improvement of SAT based Bounded Model Checking

Emmanuel Zarpas

Presented at Formal Methods in Computer-Aided Design (FMCAD 2004), Austin, Texas, November 14-17, 2004


In this paper, we show how proper benchmarking, which matches day-to-day use of formal methods, allows us to assess direct improvements for SAT use for formal methods. Proper uses of our benchmark allowed us to prove that previous results on tuning SAT solver for Bounded Model Checking (BMC) were overly optimistic and that a simpler algorithm was in fact more efficient.

START Conference Manager (V2.46.3)