Tue 9 Jan 2018 10:30 - 11:00 at Museum A - Trusted Verification Frameworks and Systems Chair(s): Zhong Shao

Based on our earlier formalization of conflict-driven clause learning (CDCL) in Isabelle/HOL, we refine the CDCL calculus to add a crucial optimization: two watched literals. We formalize the data structure and the invariants. Then we refine the calculus to obtain an executable SAT solver. Through a chain of refinements carried out using the Isabelle Refinement Framework, we target Imperative HOL and extract imperative Standard ML code. Although our solver is not competitive with the state of the art, it offers acceptable performance for some applications, and heuristics can be added to improve it further.

Tue 9 Jan

CPP-2018
10:30 - 12:00: CPP 2018 - Trusted Verification Frameworks and Systems at Museum A
Chair(s): Zhong ShaoYale University
CPP-201810:30 - 11:00
Talk
Mathias FleuryMPI-INF, Jasmin Christian BlanchetteVrije Universiteit Amsterdam, Peter LammichTechnische Universität München
DOI
CPP-201811:00 - 11:30
Talk
Eric MullenUniversity of Washington, Stuart PernsteinerUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Dan GrossmanUniversity of Washington
DOI
CPP-201811:30 - 12:00
Talk
Maria Paola BonacinaUniversity of Verona, Italy, Stéphane Graham-LengrandCNRS, France, Natarajan ShankarSRI International, USA
DOI