Adaptable Value-Set Analysis for Low-Level Code

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

doi:10.4230/OASIcs.SSV.2011.32

Document

Adaptable Value-Set Analysis for Low-Level Code

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

Part of: Volume: 6th International Workshop on Systems Software Verification (SSV 2011)
Part of: Series: Open Access Series in Informatics (OASIcs)
License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
Publication Date: 2012-07-13

PDF

File

PDF

OASIcs.SSV.2011.32.pdf

Filesize: 421 kB
12 pages

Document Identifiers

DOI: 10.4230/OASIcs.SSV.2011.32
URN: urn:nbn:de:0030-drops-35884

Subject Classification

Keywords

Abstract interpretation
SAT solving
embedded systems

Metrics

Access Statistics
Total Accesses (updated on a weekly basis)

0

PDF Downloads

0

Metadata Views

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.

Cite As Get 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

Author Details

Jörg Brauer

René Rydhof Hansen

Stefan Kowalewski

Kim G. Larsen

Mads Chr. Olesen

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