Inference of ranking functions for proving temporal properties by abstract interpretation. (January 2017)

• Record Type: Journal Article
• Authors: Urban, Caterina; Miné, Antoine
• Is Part Of: Computer languages, systems & structures. Volume 47:Part 1(2017)
• Page Start: 77
• Page End: 103
• Publication Date: 2017-01
• Subjects: Static analysis -- Abstract interpretation -- Liveness -- Temporal properties -- Ranking functions -- Termination; Programming languages (Electronic computers) -- Periodicals; Computer networks -- Periodicals; Computer architecture -- Periodicals; Computer systems -- Periodicals; Langage de programmation; Réseau d'ordinateurs; Architecture d'ordinateur; Périodique électronique (Descripteur de forme); Ressource Internet (Descripteur de forme); 005.13
• DOI: 10.1016/j.cl.2015.10.001
• Languages: English
• ISSNs: 1477-8424

Abstract

Abstract: We present new static analysis methods for proving liveness properties of programs. In particular, with reference to the hierarchy of temporal properties proposed by Manna and Pnueli, we focus on guarantee (i.e., "something good occurs at least once ") and recurrence (i.e., "something good occurs infinitely often ") temporal properties. We generalize the abstract interpretation framework for termination presented by Cousot and Cousot. Specifically, static analyses of guarantee and recurrence temporal properties are systematically derived by abstraction of the program operational trace semantics. These methods automatically infer sufficient preconditions for the temporal properties by reusing existing numerical abstract domains based on piecewise-defined ranking functions. We augment these abstract domains with new abstract operators, including a dual widening . To illustrate the potential of the proposed methods, we have implemented a research prototype static analyzer, for programs written in a C-like syntax, that yielded interesting preliminary results. Abstract : Highlights: We present new static analysis methods for proving liveness properties of programs. We generalize an existing abstract interpretation framework for termination. We reuse existing abstract domains based on piecewise-defined ranking functions. The static analyses methods infer sufficient preconditions for the liveness properties. We provide a prototype implementation of these static analyses.