Metric Spaces and Termination Analyses

We present a framework for defining abstract interpreters for liveness properties, in particular program termination. The framework makes use of the theory of metric spaces to define a concrete semantics, relates this semantics with the usual order-theoretic semantics of interpretation, and identifies a set of conditions for determining abstract interpreter is sound for analysing liveness properties. Our soundness proof of the framework is based on a novel relationship between unique fixpoints in metric semantics and post-fixpoints comabstract interpreters. We illustrate the power of the framework by providing an instance that can automatically prove the termination of programs with general (not necessarily tail) recursion.

• Type: Journal
• Year: 2010
• Where: APLAS
• Authors: Aziem Chawdhary, Hongseok Yang
• Keywords: Abstract Interpreter, APLAS 2010, Liveness Properties, Programming Languages, Semantics