IBM Logo
IBM Research Lab in Haifa
Hot Shots  
FV Research in HRL  

Download the presentation

Armando Tacella

University of Genova


A Journey into the World of SAT Solvers

The talk focuses on (i) providing some insight of state-of-the-art Davis-Longeman-Loveland (DLL) solvers and (ii) on comparing Stalmarck's calculus and DLL algorithm/calculus from an high-level perspective. The purpose is to guide the audience to a better understanding of "modern" SAT solvers, in order to see how they can be used to tackle formal verification problems.