Author | Conference | Journal | Organization | Year | DOI
Look for results that meet for the following criteria:

Keywords (1)

Academic
Publications
Automatic Abstraction for Intervals Using Boolean Formulae
Edit
Automatic Abstraction for Intervals Using Boolean Formulae   (Citations: 7)
BibTex | RIS | RefWorks Download
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.
Conference: Static Analysis Symposium/Workshop on Static Analysis - SAS(WSA) , pp. 167-183, 2010
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
More »
    • ...The seminal work of Reps and his colleagues [29] advocated the automatic synthesis of transfer functions, though recently the topic has attracted increasing attention [6,19,23] because of the desire to generate transfer functions for blocks rather than single instructions...
    • ...To derive a transfer function for interval analysis, it is necessary to ascertain how the maximal value of x � , denoted x � , relates to the minimal and maximal values of x, denoted x� and xu .T he value ofx � can be specified in logic [6,23] by asserting that: (i) for every value of x that falls in the interval [x� ,xu], the value of x � is greater or equal to x � , and (ii) for some value of x in [x� ,xu], the output x � takes the value ...
    • ...It is therefore no surprise that this approach has only been demonstrated for blocks of microcontroller code where the word-size is just 8 bits [6]...
    • ...We overcome this problem by reformulating the construction given in [6] for the synthesis of guards...
    • ...Following our initial approach [6], the transfer function for a multi-modal block (where the internal instructions can wrap) is described as a system of guarded updates...
    • ...To obtain these guards, we solve a series of SAT instances, rather than following a monolithic all-in-one approach based on quantifier elimination [6]...
    • ...By way of comparison with [6], adding a single propositional variable to a formula can increase the complexity of resolution quadratically...
    • ...Transformers over template constraints have been previously formulated using quantification [6,23]...
    • ...Moreover (M1 � M2) � M3 represents the best affine abstraction of ξ(X) [6,19]...
    • ...In our previous work [6], the application of a transfer function amounted to solving a series of integer linear programs (ILPs)...
    • ...2 compares the results for intervals for different blocks of assembly code to those obtained using the technique described in [6]...
    • ...The overall runtime of the eliminationbased algorithm [6] is given in column old (∞ is used for timeout, which is set to 30s)...
    • ...In terms of precision, the results coincide with those previously generated [6]...
    • ...Sat4J does reuse clauses learnt in an earlier SAT instances, though it does not permit clauses to be incrementally added and rescinded which is useful when solving maximisation problems [6]...
    • ...This motivates applying a decision procedure in order to compute optimal transfer functions offline, prior to the actual analysis [6,19]...
    • ...Our previous work [6] shows how bit-blasting and quantifier elimination can be applied to synthesise transformers for bit-vector programs...
    • ...The irony is that although Boolean formula initially appear attractive for synthesis because of the simplicity of universal projection [6], their real strength is the fact that they are discrete...
    • ...However, if intermediate variables y are needed to express rπ(x,x � ), p(c,x), p(c,x � )o r<, then the formula actually takes the form ∃c : ∀x : ∀x � : ∃y : ν where ∃y : ν ≡ rπ(x,x � ) → (p(c,x) <p (c,x � )). This formula is similar to those solved in [6] by elimination which begs the question of whether this problem, like that of transfer function synthesis, can be recast to avoid elimination altogether...

    Jörg Brauer, et al. Transfer Function Synthesis without Quantifier Elimination

    • ...Yet SAT remains a comparative novelty in abstract interpretation where it is more often than not relegated to solving auxiliary problems such as that of synthesising best transformers [4,20,30] rather then being integrated into the heart of the analysis itself [18]...
    • ...Projection arises when computing transfer functions [4] and, very recently, in the synthesis of ranking functions from template constraints for low-level code [10]...

    Jörg Brauer, et al. Approximate Quantifier Elimination for Propositional Boolean Formulae

    • ...Following the observation of Regehr et al. [20] that low-level code requires accurate transformers there has been increasing interest in automatically synthesizing optimal abstractions [21], [22] from the concrete semantics of a program based on SAT solving [23], [24], [25]...

    Sebastian Biallas, et al. SAT-based abstraction refinement for programmable logic controllers

    • ...For instance, determining tight bounds for the worst-case execution time of an application [12] or checking safety properties of micro-controllers [7] for flawless functionality, demand for analysing the compiler output...

    Andrea Flexeder, et al. Interprocedural Control Flow Reconstruction

    • ...Our work builds on this to remedy both the difficulty and the workload of handcrafting transfer functions for the complete instruction set of the microcontroller as in [4]...

    Jörg Brauer, et al. Range Analysis of Microcontroller Code Using Bit-Level Congruences

Order by:

Citations (7)

Share this on | Contribute to Academic