SMT (Satisfiability Modulo Theories): um cálculo para a ciência da computação

Abstract

SMT (Satisfiability Modulo Theories) consiste em checar a satisfiabilidade de formulas em lógica de primeira ordem em relação a uma ou mais teorias. O problema combina algumas das mais fundamentais áreas da ciência da computação. Ele combina o problema de satisfação Booleana (SAT) com domínios, tais como, os estudados em otimização e manipulação simbólica de termos. Ele também se beneficia dos mais prolíficos problemas estudados em lógica simbólica no ultimo século: o problema da decisão, completude e incompletude de teorias lógicas, e complexidade. O problema de combinar algoritmos específicos para um domínio é tão profundo e complexo quanto o processo de encontrar novos algoritmos que funcionem bem em problemas encontrados na indústria. SMT está presente no coração de diversas ferramentas de engenharia de software, tais como, geradores automáticos de testes, analisadores de programas, verificadores de tipo e checadores de modelo. Um provador SMT que leva em consideração os recentes avanços da área é varias ordens de magnitude mais rápido que uma solução ad-hoc.

Bio

Leonardo de Moura é um pesquisador da Microsoft Research em Redmond, EUA. Ele trabalha atualmente em dedução automática e no provador de teoremas Z3. De 2001 a 2006, ele foi um cientista da computação do SRI International em Menlo Park, EUA. Ele obteve o titulo de PhD em engenharia de software na PUC-Rio em 2000. Seus interesses incluem procedimentos de decisão, provadores automáticos de teorema e análise de software.


CategoryTalks

TecMF: TalkLeonardo2009 (last edited 2010-08-11 15:16:54 by localhost)