Título:	On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS
Autor(es):	Almeida, Ariane Alves
Orientador(es):	Ayala-Rincón, Mauricio
Coorientador(es):	Muñoz, César Augusto
Assunto:	Termination Formalization Functional programs Term rewriting sys- tems
Data de publicação:	4-nov-2021
Data de defesa:	9-jul-2021
Referência:	ALMEIDA, Ariane Alves. On Termination by Dependency Pairs and Termination of First-Order Functional Specifications in PVS. 2021. viii,120 f., il. Tese (Doutorado em Informática)—Universidade de Brasília, Brasília, 2021
Abstract:	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.
Unidade Acadêmica:	Instituto de Ciências Exatas (IE) Departamento de Ciência da Computação (IE CIC)
Informações adicionais:	Tese (doutorado)—Universidade de Brasília, Instituto de Ciências Exatas, Departamento de Ciência da Computação, 2021.
Programa de pós-graduação:	Programa de Pós-Graduação em Informática
Licença:	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.
Agência financiadora:	Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES).
Aparece nas coleções:	Teses, dissertações e produtos pós-doutorado

Os itens no repositório estão protegidos por copyright, com todos os direitos reservados, salvo quando é indicado o contrário.