Skip to main content

Automatic Abstraction for Intervals using Boolean Formulae

Brauer, Jorg and King, Andy (2010) Automatic Abstraction for Intervals using Boolean Formulae. In: Cousot, Radhia and Martel, Matthieu, eds. Static Analysis Symposium. Lecture Notes in Computer Science, 6337 . Springer-Verlag, pp. 182-196. ISBN 978-3-642-15768-4. (KAR id:30633)

Language: English
Download (237kB) Preview
Official URL


Traditionally, transfer functions have been manually designed for each operation in a program. Recently, however, there has been growing interest in computing transfer functions, motivated by the desire to reason about sequences of operations that constitute basic blocks. This paper focuses on deriving transfer functions for intervals --- possibly the most widely used numeric domain --- and shows how they can be computed from Boolean formulae which are derived through bit-blasting. This approach is entirely automatic, avoids complicated elimination algorithms, and provides a systematic way of handling wrap-arounds (integer overflows and underflows) which arise in machine arithmetic.

Item Type: Book section
Uncontrolled keywords: determinacy analysis, Craig interpolants
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing > Programming Languages and Systems Group
Faculties > Sciences > School of Computing > Security Group
Depositing User: Andy King
Date Deposited: 21 Sep 2012 09:49 UTC
Last Modified: 15 Feb 2020 04:04 UTC
Resource URI: (The current URI for this page, for reference purposes)
King, Andy:
  • Depositors only (login required):


Downloads per month over past year