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 (GMT-07:00) Tijuana, Baja California change

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 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