Certifying Termination Proofs - the Evolution of IsaFoR/CeTA Esta palestra cobrirá uma visão geral do certificador CeTA, cuja solidez foi comprovada em Isabelle/HOL. Começaremos com a fase inicial em que o CeTA foi usado exclusivamente para verificar as provas de terminação dos sistemas de reescrita de termos e, em seguida, continuaremos com os desenvolvimentos recentes que desencadearam o desenvolvimento de um solucionador SMT totalmente verificado para aritmética linear inteira.René Thiemann - Computational Logic Group University of Innsbruck em 05/11/2021 Abstract Since the early days of the termination competition, there have always been wrong answers produced by termination analysis tools. One way to increase the reliabil- ity of the generated analyses is by certification, an approach where the answers of the termination tools are checked by some verified certifier.This talk will cover an overview of the CeTA certifier, whose soundness has been proven in Isabelle/HOL. We will start with the early phase where CeTA was solely used to check termination proofs of term rewrite systems, and then continue with recent developments that triggered the development of a fully verified SMT solver for linear integer arithmetic. Local e Data Tema: Certifying Termination Proofs - the Evolution of IsaFoR/CeTAPalestrante: René Thiemann - Computational Logic Group University of InnsbruckData: 05/11/2021 Secretaria Fale ConoscoRoteiros e ProcedimentosSolicitaçõesTelefones e e-mail Seminários Álgebra Análise Geometria Mecânica Sistemas Dinâmicos Teoria da Computação Teoria da Probabilidade Teoria dos Números
