POPL 2018 (series) / CPP 2018 (series) / CPP 2018 - The 7th ACM SIGPLAN International Conference on Certified Programs and Proofs /
A Verified SAT Solver with Watched Literals Using Imperative HOL
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 JanDisplayed time zone: Tijuana, Baja California change
Tue 9 Jan
Displayed time zone: Tijuana, Baja California change
10:30 - 12:00 | |||
10:30 30mTalk | A Verified SAT Solver with Watched Literals Using Imperative HOL CPP Mathias Fleury MPI-INF, Jasmin Blanchette Vrije Universiteit Amsterdam, Peter Lammich Technische Universität München DOI | ||
11:00 30mTalk | Œuf: Minimizing the Coq Extraction TCB CPP Eric Mullen University of Washington, Stuart Pernsteiner University of Washington, USA, James R. Wilcox University of Washington, Zachary Tatlock University of Washington, Seattle, Dan Grossman University of Washington DOI | ||
11:30 30mTalk | Proofs in Conflict-Driven Theory Combination CPP Maria Paola Bonacina University of Verona, Italy, Stéphane Graham-Lengrand CNRS, France, Natarajan Shankar SRI International, USA DOI | ||