License
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://drops.dagstuhl.de/opus/volltexte/2012/3588/
Go to the corresponding 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:
Document 1.pdf (421 KB)


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 =		{http://dx.doi.org/10.4230/OASIcs.SSV.2011.32},
  annote =	{Keywords: Abstract interpretation, SAT solving, embedded systems}
}

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


DROPS-Home | Fulltext Search | Imprint Published by LZI