School of Computing

Automatic Abstraction for Intervals using Boolean Formulae

Jorg Brauer and Andy King

In Radhia Cousot and Matthieu Martel, editors, Seventeenth International Static Analysis Symposium, Lecture Notes in Computer Science, pages 182-196. Springer-Verlag, September 2010.

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.

Download publication 293 kbytes (PDF)

Bibtex Record

@inproceedings{3015,
author = {Jorg Brauer and Andy King},
title = {Automatic {A}bstraction for {I}ntervals using {B}oolean {F}ormulae},
month = {September},
year = {2010},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/2010/3015},
    publication_type = {inproceedings},
    submission_id = {20798_1277384086},
    booktitle = {Seventeenth International Static Analysis Symposium},
    editor = {Radhia Cousot and Matthieu Martel},
    series = {Lecture Notes in Computer Science},
    publisher = {Springer-Verlag},
    refereed = {yes},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014