Talks and Poster Presentations (with Proceedings-Entry):
T. Reinbacher, J. Brauer:
"Precise control flow reconstruction using boolean logic";
Talk: EMSOFT2011, ACM international conference on Embedded software,
Taipei;
2011-10-09
- 2011-10-14; in: "EMSOFT '11 Proceedings of the ninth ACM international conference on Embedded software",
ACM New York,
(2011),
ISBN: 978-1-4503-0714-7;
117
- 126.
English abstract:
This paper presents a SAT-based method for control flow graph reconstruction from executable code. The key idea of the technique is to express the semantics of each basic block in a program using Boolean logic, followed by inferring pre- and postconditions for each block through interleaved forward and backward analysis. In particular, the technique relies on register-wise value-set abstractions, which are subsequently refined using alternating forward and backward analyses. Experimental evidence shows that this approach, despite being sound, recovers the control flow graph precisely for different real-world benchmarks.
"Official" electronic version of the publication (accessed through its Digital Object Identifier - DOI)
http://dx.doi.org/10.1145/2038642.2038662
Related Projects:
Project Head Andreas Steininger:
Framework für CounterExample Validierung und Testfallgenerierung für die Verifikation von eingebetteter Software