Automatic Abstraction for Intervals Using Boolean Formulae

c Abstraction for Intervals Using Boolean Formulae J¨org Brauer1 and Andy King2 1 Embedded Software Laboratory, RWTH Aachen University, Germany 2 Portcullis Computer Security, Pinner, UK 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.

• Type: Journal
• Year: 2010
• Where: SAS
• Authors: Jörg Brauer, Andy King
• Keywords: Boolean Formulae J¨org, Formal Methods, RWTH Aachen University, SAS 2010, Transfer Functions