Please use this identifier to cite or link to this item: https://repositorio.ufrn.br/handle/123456789/17987
Full metadata record
DC FieldValueLanguage
dc.contributor.advisorDéharbe, David Boris Paulpt_BR
dc.contributor.authorOliveira, Diego Caminha Barbosa dept_BR
dc.date.accessioned2014-12-17T15:47:48Z-
dc.date.available2008-12-05pt_BR
dc.date.available2014-12-17T15:47:48Z-
dc.date.issued2007-11-07pt_BR
dc.identifier.citationOLIVEIRA, Diego Caminha Barbosa de. Deciding difference logic in a Nelson-Oppen combination framework. 2007. 71 f. Dissertação (Mestrado em Ciência da Computação) - Universidade Federal do Rio Grande do Norte, Natal, 2007.por
dc.identifier.urihttps://repositorio.ufrn.br/jspui/handle/123456789/17987-
dc.formatapplication/pdfpor
dc.languageengeng
dc.publisherUniversidade Federal do Rio Grande do Nortepor
dc.rightsAcesso Abertopor
dc.subjectDecision procedureeng
dc.subjectDifference logiceng
dc.subjectFormal methodseng
dc.subjectSMT - Solverseng
dc.subjectNelson oppeneng
dc.titleDeciding difference logic in a Nelson-Oppen combination frameworkeng
dc.typemasterThesispor
dc.publisher.countryBRpor
dc.publisher.initialsUFRNpor
dc.publisher.programPrograma de Pós-Graduação em Sistemas e Computaçãopor
dc.contributor.authorIDpor
dc.contributor.authorLatteshttp://lattes.cnpq.br/6949982320625762por
dc.contributor.advisorIDpor
dc.contributor.advisorLatteshttp://buscatextual.cnpq.br/buscatextual/visualizacv.do?id=K4768856U5por
dc.contributor.referees1Oliveira, Marcel Vinicius Medeirospt_BR
dc.contributor.referees1IDpor
dc.contributor.referees1Latteshttp://lattes.cnpq.br/1756952696097255por
dc.contributor.referees2Menz, Stephanpt_BR
dc.description.resumoO 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 relatadoseng
dc.publisher.departmentCiência da Computaçãopor
dc.subject.cnpqCNPQ::CIENCIAS EXATAS E DA TERRA::CIENCIA DA COMPUTACAO::SISTEMAS DE COMPUTACAOpor
Appears in Collections:PPGSC - Mestrado em Sistemas e Computação

Files in This Item:
File Description SizeFormat 
DiegoCBO.pdf551,58 kBAdobe PDFThumbnail
View/Open


Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.