Détection des fonctions de rang linéaires à terme

TitleDétection des fonctions de rang linéaires à terme
Publication TypeConference Paper
Year of Publication2013
AuthorsAlezan A, Bagnara R, Mesnard F, Payet É
Conference NameNeuvièmes Journées Francophones de Programmation par Contraintes (JFPC 2013)
Conference LocationAix-en-Provence, France
Keywordsranking functions, software verification, static analysis, termination analysis
Abstract

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of constraint programming. In this paper, we first recall an algorithm based on Farkas’ Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this polynomial algorithm.

File attachments: 

Eventual Linear Ranking Functions

TitleEventual Linear Ranking Functions
Publication TypeConference Paper
Year of Publication2013
AuthorsBagnara R, Mesnard F
EditorPeña R, Schrijvers T
Conference Name15th International Symposium on Principles and Practice of Declarative Programming (PPDP 2013)
Conference LocationMadrid, Spain
ISBN Number978-1-4503-2154-9
Keywordsranking functions, software verification, static analysis, termination analysis
Abstract

Program termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas’ Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

DOI10.1145/2505879.2505884
File attachments: 

Symbolic Path-Oriented Test Data Generation for Floating-Point Programs

TitleSymbolic Path-Oriented Test Data Generation for Floating-Point Programs
Publication TypeConference Paper
Year of Publication2013
AuthorsBagnara R, Carlier M, Gori R, Gotlieb A
Conference NameProceedings of the 6th IEEE International Conference on Software Testing, Verification and Validation
PublisherIEEE Press
Conference LocationLuxembourg City, Luxembourg
ISBN Number978-0-7695-4968-2/13
Keywordsfloating-point, IEEE 754, testing, verification
Abstract

Verifying critical numerical software involves the generation of test data for floating-point intensive programs. As the symbolic execution of floating-point computations presents significant difficulties, existing approaches usually resort to random or search-based test data generation. However, without symbolic reasoning, it is almost impossible to generate test inputs that execute many paths with floating-point computations. Moreover, constraint solvers over the reals or the rationals do not handle the rounding errors. In this paper, we present a new version of FPSE, a symbolic evaluator for C program paths, that specifically addresses this problem. The tool solves path conditions containing floating-point computations by using correct and precise projection functions. This version of the tool exploits an essential filtering property based on the representation of floating-point numbers that makes it suitable to generate path-oriented test inputs for complex paths characterized by floating-point intensive computations. The paper reviews the key implementation choices in FPSE and the labeling search heuristics we selected to maximize the benefits of enhanced filtering. Our experimental results show that FPSE can generate correct test inputs for selected paths containing several hundreds of iterations and thousands of executable floating-point statements on a standard machine: this is currently outside the scope of any other symbolic-execution test data generator tool.

DOI10.1109/ICST.2013.17
File attachments: 

The Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version

TitleThe Automatic Synthesis of Linear Ranking Functions: The Complete Unabridged Version
Publication TypeJournal Article
Year of Publication2012
AuthorsBagnara R, Mesnard F, Pescetti A, Zaffanella E
Abstract

The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.

URLhttp://arxiv.org/abs/1004.0944v2
File attachments: 

A New Look at the Automatic Synthesis of Linear Ranking Functions

TitleA New Look at the Automatic Synthesis of Linear Ranking Functions
Publication TypeJournal Article
Year of Publication2012
AuthorsBagnara R., Mesnard F., Pescetti A., Zaffanella E.
JournalInformation and Computation
Volume215
Pagination47-67
ISSN0890-5401
Abstract

The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many terminating loops admit one and algorithms exist to automatically synthesize it. In this paper we present two such algorithms: one based on work dated 1991 by Sohn and Van Gelder; the other, due to Podelski and Rybalchenko, dated 2004. Remarkably, while the two algorithms will synthesize a linear ranking function under exactly the same set of conditions, the former is mostly unknown to the community of termination analysis and its general applicability has never been put forward before the present paper. In this paper we thoroughly justify both algorithms, we prove their correctness, we compare their worst-case complexity and experimentally evaluate their efficiency, and we present an open-source implementation of them that will make it very easy to include termination-analysis capabilities in automatic program verifiers.

File attachments: 

Coding Guidelines for {Prolog}

TitleCoding Guidelines for {Prolog}
Publication TypeJournal Article
Year of Publication2012
AuthorsCovington MA, Bagnara R, O’Keefe RA, Wielemaker J, Price S
JournalTheory and Practice of Logic Programming
Volume12
Pagination889-927
Date Published11/2012
ISSN1471-0684
Keywordscoding standards, debugging, efficiency, Prolog, style
Abstract

Coding standards and good practices are fundamental to a disciplined approach to software projects, whatever programming languages they employ. Prolog programming can benefit from such an approach, perhaps more than programming in other languages. Despite this, no widely accepted standards and practices seem to have emerged up to now. The present paper is a first step towards filling this void: it provides immediate guidelines for code layout, naming conventions, documentation, proper use of Prolog features, program development, debugging and testing. Presented with each guideline is its rationale and, where sensible options exist, illustrations of the relative pros and cons for each alternative. A coding standard should always be selected on a per-project basis, based on a host of issues pertinent to any given programming project; for this reason the paper goes beyond the mere provision of normative guidelines by discussing key factors and important criteria that should be taken into account when deciding on a fully-fledged coding standard for the project.

DOI10.1017/S1471068411000391

Exact Join Detection for Convex Polyhedra and Other Numerical Abstractions

TitleExact Join Detection for Convex Polyhedra and Other Numerical Abstractions
Publication TypeJournal Article
Year of Publication2010
AuthorsBagnara R, Hill PM, Zaffanella E
JournalComputational Geometry: Theory and Applications
Volume43
Pagination453–473
ISSN0925-7721
Keywordsundefined
Abstract

Deciding whether the union of two convex polyhedra is itself a convex polyhedron is a basic problem in polyhedral computations; having important applications in the field of constrained control and in the synthesis, analysis, verification and optimization of hardware and software systems. In such application fields though, general convex polyhedra are just one among many, so-called, numerical abstractions, which range from restricted families of (not necessarily closed) convex polyhedra to non-convex geometrical objects. We thus tackle the problem from an abstract point of view: for a wide range of numerical abstractions that can be modeled as bounded join-semilattices –-that is, partial orders where any finite set of elements has a least upper bound–-, we show necessary and sufficient conditions for the equivalence between the lattice-theoretic join and the set-theoretic union. For the case of closed convex polyhedra –-which, as far as we know, is the only one already studied in the literature–- we improve upon the state-of-the-art by providing a new algorithm with a better worst-case complexity. The results and algorithms presented for the other numerical abstractions are new to this paper. All the algorithms have been implemented, experimentally validated, and made available in the Parma Polyhedra Library.

DOI10.1016/j.comgeo.2009.09.002
File attachments: 

Applications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems

TitleApplications of Polyhedral Computations to the Analysis and Verification of Hardware and Software Systems
Publication TypeJournal Article
Year of Publication2009
AuthorsBagnara R, Hill PM, Zaffanella E
JournalTheoretical Computer Science
Volume410
Pagination4672–4691
ISSN0304-3975
Keywordsabstract interpretation, polyhedron, software verification, static analysis
Abstract

Convex polyhedra are the basis for several abstractions used in static analysis and computer-aided verification of complex and sometimes mission critical systems. For such applications, the identification of an appropriate complexity-precision trade-off is a particularly acute problem, so that the availability of a wide spectrum of alternative solutions is mandatory. We survey the range of applications of polyhedral computations in this area; give an overview of the different classes of polyhedra that may be adopted; outline the main polyhedral operations required by automatic analyzers and verifiers; and look at some possible combinations of polyhedra with other numerical abstractions that have the potential to improve the precision of the analysis. Areas where further theoretical investigations can result in important contributions are highlighted.

DOI10.1016/j.tcs.2009.07.033
File attachments: 

Weakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness

TitleWeakly-Relational Shapes for Numeric Abstractions: Improved Algorithms and Proofs of Correctness
Publication TypeJournal Article
Year of Publication2009
AuthorsBagnara R, Hill PM, Zaffanella E
JournalFormal Methods in System Design
Volume35
Pagination279–323
ISSN0925-9856
Keywordsabstract interpretation, integer constraints, octagonal constraints, software verification, static analysis, unit two variables per inequality constraints, UTVPI constraints
Abstract

Weakly-relational numeric constraints provide a compromise between complexity and expressivity that is adequate for several applications in the field of formal analysis and verification of software and hardware systems. We address the problems to be solved for the construction of full-fledged, efficient and provably correct abstract domains based on such constraints. We first propose to work with semantic abstract domains, whose elements are geometric shapes, instead of the (more concrete) syntactic abstract domains of constraint networks and matrices on which the previous proposals are based. This allows to solve, once and for all, the problem whereby closure by entailment, a crucial operation for the realization of such domains, seemed to impede the realization of proper widening operators. In our approach, the implementation of widenings relies on the availability of an effective reduction procedure for the considered constraint description: one for the domain of bounded difference shapes already exists in the literature; we provide algorithms for the significantly more complex cases of rational and integer octagonal shapes. We also improve upon the state-of-the-art by presenting, along with their proof of correctness, closure by entailment algorithms of reduced complexity for domains based on rational and integer octagonal constraints. The consequences of implementing weakly-relational numerical domains with floating point numbers are also discussed.

DOI10.1007/s10703-009-0073-1
File attachments: 

An Improved Tight Closure Algorithm for Integer Octagonal Constraints

TitleAn Improved Tight Closure Algorithm for Integer Octagonal Constraints
Publication TypeConference Paper
Year of Publication2008
AuthorsBagnara R, Hill PM, Zaffanella E
EditorLogozzo F, Peled D, Zuck L
Conference NameVerification, Model Checking and Abstract Interpretation: Proceedings of the 9th International Conference (VMCAI 2008)
PublisherSpringer Berlin / Heidelberg
Conference LocationSan Francisco, CA, USA
ISBN Number3-540-78162-2
Keywordsabstract interpretation, numerical properties, software verification, static analysis, unit two variables per inequality integer constraints, UTVPI integer constraints
Abstract

Integer octagonal constraints(a.k.a.\ Unit Two Variables Per Inequality or UTVPI integer constraints) constitute an interesting class of constraints for the representation and solution of integer problems in the fields of constraint programming and formal analysis and verification of software and hardware systems, since they couple algorithms having polynomial complexity with a relatively good expressive power. The main algorithms required for the manipulation of such constraints are the satisfiability check and the computation of the inferential closure of a set of constraints. The latter is called tight closure to mark the difference with the (incomplete) closure algorithm that does not exploit the integrality of the variables. In this paper we present and fully justify an O(n^3) algorithm to compute the tight closure of a set of UTVPI integer constraints.

DOI10.1007/978-3-540-78163-9_6
File attachments: