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,
- 2011-10-14; in: "EMSOFT '11 Proceedings of the ninth ACM international conference on Embedded software",
ACM New York,
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)
Project Head Andreas Steininger:
Framework für CounterExample Validierung und Testfallgenerierung für die Verifikation von eingebetteter Software
Created from the Publication Database of the Vienna University of Technology.