2026-07-24T10:14:54Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:3588 2024-03-06T10:29:02Z ddc:004 open_access

Adaptable Value-Set Analysis for Low-Level Code Brauer, Jörg Hansen, René Rydhof Kowalewski, Stefan Larsen, Kim G. Olesen, Mads Chr. Abstract interpretation SAT solving embedded systems 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Jörg Brauer and René Rydhof Hansen and Stefan Kowalewski and Kim G. Larsen and Mads Chr. Olesen 2012 Is Part Of OASIcs, Volume 24, 6th International Workshop on Systems Software Verification (2012) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/OASIcs.SSV.2011.32 urn:nbn:de:0030-drops-35884 https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.SSV.2011.32 eng https://creativecommons.org/licenses/by-nc-nd/3.0/legalcode