Uma banca de DEFESA de DOUTORADO foi cadastrada pelo programa.
DATA : 05/09/2017
HORA: 09:00
LOCAL: Sala C005, LORIA, Nancy, FR

New techniques for instantiation and proof production in SMT solving


quantifier instantiation, proof production, proof automation, smt solving, formal verification

GRANDE ÁREA: Ciências Exatas e da Terra
ÁREA: Ciência da Computação
SUBÁREA: Metodologia e Técnicas da Computação
ESPECIALIDADE: Engenharia de Software
A variety of real world applications, such as formal verification, program synthesis, automatic testing, and program analysis, rely on satisfiability modulo theories (SMT) solvers as backends to automatically discharge proof obligations. While these solvers are extremely efficient at handling large ground formulas with theory symbols, such as arithmetic ones, they still struggle to deal with quantifiers.

Our first contribution in this thesis is in providing a uniform and efficient framework for reasoning with quantified formulas in CDCL(T), the calculus more commonly used in SMT solvers, in which generally various instantiation techniques are employed to handle quantifiers.  We show that the major instantiation techniques can be all cast in a unifying framework for quantified formulas with equality and uninterpreted functions. This framework is based on the problem of E-ground (dis)unification, a variation of the classic rigid E-unification problem.  We introduce a sound and complete calculus to solve this problem in practice: Congruence Closure with Free Variables (CCFV). An experimental evaluation of the implementation of CCFV in the SMT solver veriT validates the approach. veriT exhibits significant improvements and is now competitive with state-of-the-art solvers in several benchmark libraries stemming from real world applications.

Our second contribution is a framework for processing formulas in SMT solvers, with generation of detailed proofs. Our goal is to increase the reliability on the results of automated reasoning systems, by providing justifications which can be efficiently checked independently, and to improve their usability by external applications. Proof assistants, for instance, generally require the reconstruction of the justification provided by the solver in a given proof obligation.

The main components of our proof-producing framework are a generic contextual recursion algorithm and an extensible set of inference rules. Clausification, skolemization, theory-specific simplifications, and expansion of ‘let’ expressions are instances of this framework. With suitable data structures, proof generation adds only a linear-time overhead, and proofs can be checked in linear time. We also implemented the approach in veriT. This allowed us to dramatically simplify the code base while increasing the number of problems for which detailed proofs can be produced.

Interno - 1517271 - JOAO MARCOS DE ALMEIDA
Interno - 2220777 - DAVID BORIS PAUL DEHARBE
Externo à Instituição - ERIKA ÁBRAHÁM - RWTH
Externo à Instituição - PASCAL FONTAINE - UL
Externo à Instituição - PHILIPP RÜMMER - UU
Externo à Instituição - ANDREW REYNOLDS - UIOWA
Externo à Instituição - STEPHAN MERZ - UL
Externo à Instituição - CATHERINE DUBOIS - ENSIIE
Notícia cadastrada em: 14/09/2017 14:10
SIGAA | Superintendência de Informática - | | Copyright © 2006-2020 - UFRN -