License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/OASIcs.SSV.2011.32
URN: urn:nbn:de:0030-drops-35884
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2012/3588/
Go to the corresponding OASIcs Volume Portal

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

Adaptable Value-Set Analysis for Low-Level Code

pdf-format:
4.pdf (0.4 MB)

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.

BibTeX - Entry

@InProceedings{brauer_et_al:OASIcs:2012:3588,
  author =	{J{\"o}rg Brauer and Ren{\'e} Rydhof Hansen and Stefan Kowalewski and Kim G. Larsen and Mads Chr.  Olesen},
  title =	{{Adaptable Value-Set Analysis for Low-Level Code}},
  booktitle =	{6th International Workshop on Systems Software Verification},
  pages =	{32--43},
  series =	{OpenAccess Series in Informatics (OASIcs)},
  ISBN =	{978-3-939897-36-1},
  ISSN =	{2190-6807},
  year =	{2012},
  volume =	{24},
  editor =	{J{\"o}rg Brauer and Marco Roveri and Hendrik Tews},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2012/3588},
  URN =		{urn:nbn:de:0030-drops-35884},
  doi =		{10.4230/OASIcs.SSV.2011.32},
  annote =	{Keywords: Abstract interpretation, SAT solving, embedded systems}
}

Keywords: Abstract interpretation, SAT solving, embedded systems
Collection: 6th International Workshop on Systems Software Verification
Issue Date: 2012
Date of publication: 13.07.2012

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI