NATIONAL INSTITUTE OF AEROSPACE

9.9.16 Almeida

9.9.16 Almeida

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.

BUSINESS WITH NIA

Headquarters

100 Exploration Way
Hampton, VA 23666
(757)325-6700
www.nianet.org