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
Times are displayed in time zone: Tijuana, Baja California change

10:30 - 12:00
Trusted Verification Frameworks and SystemsCPP at Museum A
Chair(s): Zhong ShaoYale University
10:30
30m
Talk
A Verified SAT Solver with Watched Literals Using Imperative HOL
CPP
Mathias FleuryMPI-INF, Jasmin BlanchetteVrije Universiteit Amsterdam, Peter LammichTechnische Universität München
DOI
11:00
30m
Talk
Œuf: Minimizing the Coq Extraction TCB
CPP
Eric MullenUniversity of Washington, Stuart PernsteinerUniversity of Washington, USA, James R. WilcoxUniversity of Washington, Zachary TatlockUniversity of Washington, Seattle, Dan GrossmanUniversity of Washington
DOI
11:30
30m
Talk
Proofs in Conflict-Driven Theory Combination
CPP
Maria Paola BonacinaUniversity of Verona, Italy, Stéphane Graham-LengrandCNRS, France, Natarajan ShankarSRI International, USA
DOI