• Home
• Teaching
• Research
• Publications

Finiteness analyses are compile-time techniques to determine (sufficient) conditions for the finiteness of relations computed during the bottom-up execution of a logic program. We examine finiteness analyses from the perspective of abstract interpretation. However, problems arise when trying to use standard abstract interpretation theory for finiteness analysis. They occur because finiteness is not an admissible property and so naive application of abstract interpretation leads to incorrect analyses. Here we develop three simple techniques based on abstract interpretation theory which allow inadmissible properties to be handled. Existing approaches to finiteness analysis may be explained and compared in terms of our extension to abstract interpretation theory, and we claim that their correctness is more easily argued in it. To support our claim we use our techniques to develop and prove correct a finiteness analysis which is more accurate than any that we are aware of.