Adaptable Value-Set Analysis for Low-Level Code

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

Thumbnail 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)


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.
  • Abstract interpretation
  • SAT solving
  • embedded systems


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

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail