OASIcs.SSV.2011.32.pdf
- Filesize: 421 kB
- 12 pages
Document
Adaptable Value-Set Analysis for Low-Level Code
Authors
-
Part of:
Volume:
6th International Workshop on Systems Software Verification (SSV 2011)
Series: Open Access Series in Informatics (OASIcs) - License:
Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license
- Publication Date: 2012-07-13
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
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.
Subject Classification
Keywords
- Abstract interpretation
- SAT solving
- embedded systems
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads