Atenção: Todas as denúncias são sigilosas e sua identidade será preservada.
Os campos nome e e-mail são de preenchimento opcional
Metadados | Descrição | Idioma |
---|---|---|
Autor(es): dc.contributor | Ayala-Rincón, Mauricio | - |
Autor(es): dc.contributor | Muñoz, César Augusto | - |
Autor(es): dc.creator | Almeida, Ariane Alves | - |
Data de aceite: dc.date.accessioned | 2024-07-22T12:23:59Z | - |
Data de disponibilização: dc.date.available | 2024-07-22T12:23:59Z | - |
Data de envio: dc.date.issued | 2021-11-03 | - |
Data de envio: dc.date.issued | 2021-11-03 | - |
Data de envio: dc.date.issued | 2021-11-03 | - |
Data de envio: dc.date.issued | 2021-07-09 | - |
Fonte completa do material: dc.identifier | https://repositorio.unb.br/handle/10482/42296 | - |
Fonte: dc.identifier.uri | http://educapes.capes.gov.br/handle/capes/802823 | - |
Descrição: dc.description | Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2021. | - |
Descrição: dc.description | Embora indecidível, terminação é uma propriedade muito importante relacionada à cor- reção de objetos computacionais. Ela garante que para cada entrada, não haverá execução infinita, ou seja, a execução deve parar e fornecer algum resultado. Esta propriedade per- mite, por exemplo, raciocinar sobre a correção de programas, uma vez que garantir que alguma propriedade seja válida para cada saída depende da obtenção de uma saída a ser verificada sempre que uma entrada for fornecida. Ao longo dos anos, várias estratégias de semidecisão foram usadas para abordar esse problema e raciocinar sobre ele. No contexto de Programas Funcionais (FPs), por exemplo, a análise pode ser feita por meio dos Gráfi- cos de Contexto de Chamada, e no contexto de Sistemas de Reescrita de Termos (TRSs), podem ser usados Pares Dependentes. Este trabalho formaliza o Critério de Terminação por Pares Dependentes (Mais Inter- nos), um critério muito conhecido para análise de terminação de TRSs, no assistente de prova PVS. PVS é um assistente de prova com uma linguagem de especificação funcional que permite lógica de ordem superior e realiza provas seguindo o Cálculo de Sequentes de Gentzen. Também são apresentados vários Critérios de terminação formalizados para FPs em uma linguagem simplificada que modela especificações em PVS (chamada PVS0) e a formalização da equivalência entre eles, permitindo automação de provas de terminação de especificações de funções recursivas de primeira ordem em PVS. O trabalho também discute a possibilidade de navegar entre os critérios de terminação para TRSs e FPs com o objetivo de aprimorar a automação para verificar terminação. | - |
Descrição: dc.description | Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES). | - |
Descrição: dc.description | Although undecidable, termination is a very important property related to the correct- ness of computational objects. It ensures that for every input, there will be no infinite execution, i.e., the execution must stop and provide some result. This property allows, for instance, reason about correctness of programs, since to guarantee that some prop- erty hold for every output depends on obtaining an output to be analysed whenever an input is provided. Through the years, several semi-decision strategies have been used to address such problem and reason over it. In the context of Functional Programs (FPs), for instance, the analysis can be done through the Calling Context Graphs, and in the context of Term Rewriting Systems (TRSs), Dependency Pairs can be used. This work formalizes the (Innermost) Dependency Pairs Termination Criterion, a very well-known criteria for analyzing termination of TRSs, in the proof assistant PVS. PVS is a proof assistant with a functional specification language that allows higher order logic and performs proofs following the Gentzen Calculus of Sequents. It is also presented several termination criteria formalized for FPs in a simplified language modeling PVS specifications (called PVS0) and the formalization of the equivalence between them, al- lowing automation for proving termination of recursive functions first-order specification in PVS. The work also discusses the possibility of navigating between the termination criteria for TRSs to FPs aiming to improve automation of verification for termination. | - |
Formato: dc.format | application/pdf | - |
Direitos: dc.rights | Acesso Aberto | - |
Direitos: dc.rights | A concessão da licença deste item refere-se ao termo de autorização impresso assinado pelo autor com as seguintes condições: Na qualidade de titular dos direitos de autor da publicação, autorizo a Universidade de Brasília e o IBICT a disponibilizar por meio dos sites www.bce.unb.br, www.ibict.br, http://hercules.vtls.com/cgi-bin/ndltd/chameleon?lng=pt&skin=ndltd sem ressarcimento dos direitos autorais, de acordo com a Lei nº 9610/98, o texto integral da obra disponibilizada, conforme permissões assinaladas, para fins de leitura, impressão e/ou download, a título de divulgação da produção científica brasileira, a partir desta data. | - |
Palavras-chave: dc.subject | Termination | - |
Palavras-chave: dc.subject | Formalization | - |
Palavras-chave: dc.subject | Functional programs | - |
Palavras-chave: dc.subject | Term rewriting sys- tems | - |
Título: dc.title | On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS | - |
Aparece nas coleções: | Repositório Institucional – UNB |
O Portal eduCAPES é oferecido ao usuário, condicionado à aceitação dos termos, condições e avisos contidos aqui e sem modificações. A CAPES poderá modificar o conteúdo ou formato deste site ou acabar com a sua operação ou suas ferramentas a seu critério único e sem aviso prévio. Ao acessar este portal, você, usuário pessoa física ou jurídica, se declara compreender e aceitar as condições aqui estabelecidas, da seguinte forma: