Spelling suggestions: "subject:"aelson open"" "subject:"aelson öppen""
1 |
Combinaison de Méthodes de VérificationZucchelli, Daniele 22 January 2008 (has links) (PDF)
La thèse étudie des problèmes de vérification de modèles infini, en appliquant des techniques de combinaisons de solveurs de contraintes.
|
2 |
Deciding difference logic in a Nelson-Oppen combination frameworkOliveira, Diego Caminha Barbosa de 07 November 2007 (has links)
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
|
Page generated in 0.0687 seconds