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. (Full text available)

PDF
Download (233kB) Preview
[img]
Preview
Official URL
http://www.cs.kent.ac.uk/pubs/2010/3015

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: Faculties > Science Technology and Medical Studies > School of Computing > Programming Languages and Systems Group
Faculties > Science Technology and Medical Studies > School of Computing > Security Group
Depositing User: Andy King
Date Deposited: 21 Sep 2012 09:49
Last Modified: 12 Dec 2013 13:15
Resource URI: http://kar.kent.ac.uk/id/eprint/30633 (The current URI for this page, for reference purposes)
  • Depositors only (login required):

Downloads

Downloads per month over past year