Automation of Termination

This talk will present current research on automation of termination for a functional language model in the Prototype Verification System PVS.  Automatically verifying termination increases flexibility of deductive systems and compilers, and involves research challenges that range from proving fundamental theorems about the pertinence of the model to developing mechanical proofs of the correspondence of different termination criteria that were developed for several computational frameworks such as Turing machines and rewriting systems.

Mauricio Ayala-Rincón

Full Professor - Depts. C. Computação & Matemática

Universidade de Brasília, Ed. EST/CIC