Inferring congruence equations using SAT

    Thumbnail
    Citations
    Scopus
    Altmetric
    10
    Author
    King, A; SONDERGAARD, H
    Editor
    Gupta, A; Malik, S
    Date
    2008
    Source Title
    Lecture Notes in Computer Science
    Publisher
    Springer Berlin Heidelberg
    University of Melbourne Author/s
    Sondergaard, Harald
    Affiliation
    Computer Science and Software Engineering
    Metadata
    Show full item record
    Document Type
    Conference Paper
    Citations
    King, A. & SONDERGAARD, H. (2008). Inferring congruence equations using SAT. Gupta, A (Ed.) Malik, S (Ed.) Computer Aided Verification (Lecture Notes in Computer Science), 5123, pp.281-293. Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-540-70545-1_26.
    Access Status
    This item is currently not available from this repository
    URI
    http://hdl.handle.net/11343/31654
    DOI
    10.1007/978-3-540-70545-1_26
    Abstract
    This paper proposes a new approach for deriving invariants that are systems of congruence equations where the modulo is a power of 2. The technique is an amalgam of SAT-solving, where a propositional formula is used to encode the semantics of a basic block, and abstraction, where the solutions to the formula are systematically combined and summarised as a system of congruence equations. The resulting technique is more precise than existing congruence analyses since a single optimal transfer function is derived for a basic block as a whole.
    Keywords
    Computer Software

    Export Reference in RIS Format     

    Collections