Navigation

• Education
  • International programmes
  • Faculties
  • ECTS
  • Vision and policy
• Research
  • Research at KU Leuven
  • Support and funding
  • Industry and Society
  • Phd
  • Postdoc researcher
  • Output and impact
  • Networking
  • Vision and policy
• Admissions
  • How to apply
  • Scholarships
  • Degree seeking students
  • Non-degree seeking students
  • Doctoral students
  • Reseachers
  • Short term study visits
  • Prepare your stay
• Living in Leuven
  • Welcome activities
  • News and agenda
  • Student Services
  • Housing
  • Insurance
  • Sports and culture
  • Student organisations
• About KU Leuven
  • Mission statement
  • Facts and figures
  • International networks
  • Development Cooperation
  • Academic Calendar
  • Alumni
  • Fundraising
  • Services and support
  • Boards and councils
  • News and press
  • Jobs

CW 222

S. Decorte, D. De Schreye and M Fabris
Integrating types in abstract interpretation based automatic termination anaysis of logic programs

Abstract

Types are receiving increasing attention in logic programming languages. Several new languages, such as Gödel and Mercury, are typed languages. Also, the more recent Prolog systems either support and exploit optional type declarations, or perform type inference at compile time, with the purpose of verification and code-optimisation. Research in program verification, especially on termination analysis, has followed this development. In recent termination analysis works, the added power of including type information in the analysis has been demonstrated.

In this paper, we further clarify the role of types in termination analysis, with an emphasis on automation. Our main contribution is on the automatic generation of appropriate well-founded mappings (based on norms) for proving termination of a given program and (class of) queries. We propose two different approaches, which both exploit type information. A first approach infers one semi-linear norm from the given types. The second approach is more refined. It infers a set of generalised norms, referred to as typed norms. The generalisation involved in typed norms, is that the way in which a term is measured under such norms is parametrised with respect to the specific type to which the term is considered to belong.

The first approach has the advantage that it is compatible with several existing techniques for termination analysis and therefore, can be combined with them without difficulty. The second approach is strictly more refined and achieves higher precision, but it requires that part of the termination analysis -- specifically: inference of interargument or size relations -- needs to be redesigned. We develop an appropriately extended technique for inferring such relations, based on bottom-up abstract interpretation.

All parts of the proposed analysis are fully automatable and a prototype system has been implemented. A report on extensive testing performed with this system is included.