A sound floating-point polyhedra abstract domain

Liqian Chen, Antoine Miné, Patrick Cousot

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

The polyhedra abstract domain is one of the most powerful and commonly used numerical abstract domains in the field of static program analysis based on abstract interpretation. In this paper, we present an implementation of the polyhedra domain using floating-point arithmetic without sacrificing soundness. Floating-point arithmetic allows a compact memory representation and an efficient implementation on current hardware, at the cost of some loss of precision due to rounding. Our domain is based on a constraint-only representation and employs sound floating-point variants of Fourier-Motzkin elimination and linear programming. The preliminary experimental results of our prototype are encouraging. To our knowledge, this is the first time that the polyhedra domain is adapted to floating-point arithmetic in a sound way.

Original languageEnglish (US)
Title of host publicationProgramming Languages and Systems - 6th Asian Symposium, APLAS 2008, Proceedings
Pages3-18
Number of pages16
DOIs
StatePublished - 2008
Event6th Asian Symposium on Programming Languages and Systems, APLAS 2008 - Bangalore, India
Duration: Dec 9 2008Dec 11 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5356 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other6th Asian Symposium on Programming Languages and Systems, APLAS 2008
CountryIndia
CityBangalore
Period12/9/0812/11/08

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'A sound floating-point polyhedra abstract domain'. Together they form a unique fingerprint.

Cite this