Adaptable Value-Set Analysis for Low-Level Code

Authors Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, Mads Chr. Olesen



PDF
Thumbnail PDF

File

OASIcs.SSV.2011.32.pdf
  • Filesize: 421 kB
  • 12 pages

Document Identifiers

Author Details

Jörg Brauer
René Rydhof Hansen
Stefan Kowalewski
Kim G. Larsen
Mads Chr. Olesen

Cite AsGet BibTex

Jörg Brauer, René Rydhof Hansen, Stefan Kowalewski, Kim G. Larsen, and Mads Chr. Olesen. Adaptable Value-Set Analysis for Low-Level Code. In 6th International Workshop on Systems Software Verification. Open Access Series in Informatics (OASIcs), Volume 24, pp. 32-43, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)
https://doi.org/10.4230/OASIcs.SSV.2011.32

Abstract

This paper presents a framework for binary code analysis that uses only SAT-based algorithms. Within the framework, incremental SAT solving is used to perform a form of weakly relational value-set analysis in a novel way, connecting the expressiveness of the value sets to computational complexity. Another key feature of our framework is that it translates the semantics of binary code into an intermediate representation. This allows for a straightforward translation of the program semantics into Boolean logic and eases the implementation efforts, too. We show that leveraging the efficiency of contemporary SAT solvers allows us to prove interesting properties about medium-sized microcontroller programs.
Keywords
  • Abstract interpretation
  • SAT solving
  • embedded systems

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail