Termination analysis and call graph construction for higher-order functional programs

Add to your list(s) Download to your calendar using vCal

• Damien Sereni (University of Oxford)
• Friday 22 June 2007, 15:15-16:15
• GS15, Computer Laboratory.

If you have a question about this talk, please contact Viktor Vafeiadis.

Termination analysis for functional programs is a challenging problem with applications in program verification, as well as theorem proving in which it is essential to prove termination of functions for soundness. Building on the size-change termination framework proposed by Lee, Jones and Ben-Amram, we introduce termination analysis for higher-order functional programs, based on a simple but effective termination criterion.

The analysis and verification of higher-order programs raises the issue of control-flow analysis for higher-order languages. The problem of constructing an accurate call graph for a higher-order program has been the topic of extensive research, and the precision of the call graph crucially determines the precision of the resulting analysis. Our termination framework allows the call graph construction technique to be varied, and we present three constructions varying in precision and complexity.

There is to date little theoretical understanding of the precision of control-flow analyses. We use the expressiveness of termination analysis for each call graph to compare our control-flow analysis, and show that precise relationships between the classes of programs recognised as terminating by the same termination criterion over different call graph analyses. This provides a stepping stone to a better understanding of flow analyses for higher-order programs.

This talk is part of the Computer Laboratory Programming Research Group Seminar series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Programming Research Group Seminar
• Department of Computer Science and Technology talks and seminars
• GS15, Computer Laboratory
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.