Transfer Function Synthesis without Quantifier Elimination (long version)

Article English OPEN
Brauer, Jorg ; King, Andy (2012)
  • Subject: QA76

Traditionally, transfer functions have been designed manually for each operation in a program, instruction by instruction. In such a setting, a transfer function describes the semantics of a single instruction, detailing how a given abstract input state is mapped to an abstract output state. The net effect of a sequence of instructions, a basic block, can then be calculated by composing the transfer functions of the constituent instructions. However, precision can be improved by applying a single transfer function that captures the semantics of the block as a whole. Since blocks are program-dependent, this approach necessitates automation. There has thus been growing interest in computing transfer functions automatically, most notably using techniques based on quantifier elimination. Although conceptually elegant, quantifier elimination inevitably induces a computational bottleneck, which limits the applicability of these methods to small blocks. This paper contributes a method for calculating transfer functions that finesses quantifier elimination altogether, and can thus be seen as a response to this problem. The practicality of the method is demonstrated by generating transfer functions for input and output states that are described by linear template constraints, which include intervals and octagons.
  • References (89)
    89 references, page 1 of 9

    [1] Atmel Products. AVR32 Architecture Manual, 2007. http://www.atmel.com/.

    [2] R. Bagnara, P. M. Hill, and E. Zaffanella. Weakly-relational shapes for numeric abstractions: improved algorithms and proofs of correctness. Formal Methods in System Design, 35(3):279-323, 2009.

    [3] R. Bagnara, E. Rodr´ıguez-Carbonell, and E. Zaffanella. Generation of Basic Semi-algebraic Invariants Using Convex Polyhedra. In SAS, volume 3672 of LNCS, pages 19-34. Springer, 2005.

    [4] C. Baier and J.-P. Katoen. Principles of Model Checking. The MIT Press, 2008.

    [5] G. Balakrishnan. WYSINWYX: What You See Is Not What You eXecute. PhD thesis, Computer Sciences Department, University of Wisconsin, Madison, Wisconsin, USA, August 2007.

    [6] G. Balakrishnan and T. Reps. WYSINWYX: What You See Is Not What You eXecute. ACM Trans. Program. Lang. Syst., 32(6), 2010.

    [7] S. Bardin and P. Herrmann. Structural Testing of Executables. In ICST, pages 22-31. IEEE Computer Society, 2008.

    [8] S. Bardin and P. Herrmann. OSMOSE: Automatic Structural Testing of Executables. Softw. Test., Verif. Reliab., 21(1):29-54, 2011.

    [9] S. Bardin, P. Herrmann, J. Leroux, O. Ly, R. Tabary, and A. Vincent. The BINCOA Framework for Binary Code Analysis. In CAV, volume 6806 of LNCS, pages 165-170. Springer, 2011.

    [10] C. Barrett, R. Sebastiani, S. A. Seshia, and C. Tinelli. Handbook of Satisfiability, chapter Satisfiability Modulo Theories, pages 737-797. IOS Press, 2009.

  • Similar Research Results (1)
  • Metrics
    0
    views in OpenAIRE
    0
    views in local repository
    12
    downloads in local repository

    The information is available from the following content providers:

    From Number Of Views Number Of Downloads
    Kent Academic Repository - IRUS-UK 0 12
Share - Bookmark