Statically checking termination

Although it is well-known that termination is an undecidable property of programs, there are several efforts related with automating the termination of specifications with two main objectives: to develop compilers that might provide warnings of possible non-termination and to increase the grade of automation of proof assistants and deductive systems. In this talk, a general view will be given of the (Prototype Verification System) PVS theories for automating termination developed by members of the Group of Theory of Computation at the Universidade de Brasília and collaborators.