Banca de QUALIFICAÇÃO: HANIEL MOREIRA BARBOSA

Uma banca de QUALIFICAÇÃO de DOUTORADO foi cadastrada pelo programa.
DISCENTE : HANIEL MOREIRA BARBOSA
DATA : 06/07/2017
HORA: 09:00
LOCAL: Auditório 2 do DIMAp
TÍTULO:

New techniques for instantiation and proof production in SMT solving


PALAVRAS-CHAVES:

Formal verification; automatic proof techiques; SMT solving; quantifier instantiation; proof production


PÁGINAS: 100
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
RESUMO:
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
handling 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 exhibits significant improvements for the latter, making it
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 gen-
eration 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.

MEMBROS DA BANCA:
Presidente - 2220777 - DAVID BORIS PAUL DEHARBE
Interno - 1517271 - JOAO MARCOS DE ALMEIDA
Interno - 1639701 - MARCEL VINICIUS MEDEIROS OLIVEIRA
Externo à Instituição - PASCAL FONTAINE - UL
Notícia cadastrada em: 16/06/2017 10:10
SIGAA | Superintendência de Tecnologia da Informação - (84) 3342 2210 | Copyright © 2006-2024 - UFRN - sigaa06-producao.info.ufrn.br.sigaa06-producao