La thèse étudie des problèmes de vérification de modèles infini, en appliquant des techniques de combinaisons de solveurs de contraintes.

Made available in DSpace on 2014-12-17T15:47:48Z (GMT). No. of bitstreams: 1 DiegoCBO.pdf: 564820 bytes, checksum: eedd81c1881d60fea03c3dcdd8556734 (MD5) Previous issue date: 2007-11-07 / O m?todo de combina??o de Nelson-Oppen permite que v?rios procedimentos de decis?o, cada um projetado para uma teoria espec?fica, possam ser combinados para inferir sobre teorias mais abrangentes, atrav?s do princ?pio de propaga??o de igualdades. Provadores de teorema baseados neste modelo s?o beneficiados por sua caracter?stica modular e podem evoluir mais facilmente, incrementalmente. Difference logic ? uma subteoria da aritm?tica linear. Ela ? formada por constraints do tipo x − y ≤ c, onde x e y s?o vari?veis e c ? uma constante. Difference logic ? muito comum em v?rios problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em v?rios outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que v?rios algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decis?o para difference logic ? capaz de induzir sobre milhares de constraints. Um procedimento de decis?o para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic ? satisfat?vel (as vari?veis podem assumir valores que tornam o conjunto consistente) ou n?o. Al?m disso, para funcionar em um modelo de combina??o baseado em Nelson-Oppen, o procedimento de decis?o precisa ter outras funcionalidades, como gera??o de igualdade de vari?veis, prova de inconsist?ncia, premissas, etc. Este trabalho apresenta um procedimento de decis?o para a teoria de difference logic dentro de uma arquitetura baseada no m?todo de combina??o de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi poss?vel observar o seu funcionamento. Detalhes de implementa??o e testes experimentais s?o relatados