Title: Formal Methods Seminar: “Automating Termination Proofs in PVS”
Speaker: Ariane Alves Almeida, NIA visitor and PhD Candidate, University of Brasilia, Brazil
Date: Friday, September 9, 2016
Time: 11:00am
Location: NASA/LaRC, B1220, R110
Host: Cesar Munoz, NASA/LaRC
Abstract: Each time a recursive function is specified in PVS, a decreasing measure over its arguments must be provided such that the generated termination conditions assert that the function is total. In order to prove termination, another approach, different that the native one provided by PVS, can be used where the recursive function is translated into a equivalent one in a minimal functional language. In this minimal functional language, a semantic notion of termination is defined based on the existence of a finite number of recursive calls. This alternative approach, which is equivalent to PVS native approach, is also proven to be equivalent to a termination criterion on graphs, which in most practical cases can be automatically checked. This talks provides an overview of this approach, which is fully formalized in PVS, and illustrates it with a basic example.