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

Search-based satisfiability procedures try to construct a model of the input formula by simultaneously proposing candidate models and deriving new formulae implied by the input. When the formulae are satisfiable, these procedures generate a model as a witness. Dually, it is desirable to have a proof when the formulae are unsatisfiable. Conflict-driven procedures perform nontrivial inferences only when resolving conflicts between the formulae and assignments representing the candidate model. CDSAT (Conflict-Driven SATisfiability) is a method for conflict-driven reasoning in combinations of theories. It combines solvers for individual theories as theory modules within a solver for the union of the theories. In this paper we endow CDSAT with lemma learning and proof generation. For the latter, we present two techniques. The first one produces proof objects in memory: it assumes that all theory modules produce proof objects and it accommodates multiple proof formats. The second technique adapts the LCF approach to proofs from interactive theorem proving to conflict-driven SMT-solving and theory combination, by defining a small kernel of reasoning primitives that guarantees that CDSAT proofs are correct by construction.

Tue 9 Jan

Displayed time zone: Tijuana, Baja California change

10:30 - 12:00
Trusted Verification Frameworks and SystemsCPP at Museum A
Chair(s): Zhong Shao Yale University
10:30
30m
Talk
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
30m
Talk
Œ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
30m
Talk
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