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)

Abstract

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: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Andy King
Date Deposited: 21 Sep 2012 09:49 UTC
Last Modified: 16 Nov 2021 10:08 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/30633 (The current URI for this page, for reference purposes)

University of Kent Author Information

  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.