Construction of Control Flow Graphs for Binary Programs Dominik Klumpp (University of Augsburg, the Technical University Munich and the Ludwig-Maximilians-University Munich) Franck Cassez (Macquarie University) Abstract: Binary code is a low-level machine code representation of programs that can be directly executed by the hardware. Establishing qualitative properties (e.g. no stack overflow) or quantitative properties (typically worst-case execution time) of binary code is notoriously hard mostly because the code is unstructured and can contain indirect jumps (gotos) the target address of those are only know at runtime. As a result standard software analysis techniques that rely on the availability of the control flow graph of a program cannot be directly applied to the analysis of binary code. In this work, we address the problem of constructing control flow graphs (CFG) for binary programs. We introduce a novel technique inspired by trace abstraction refinement to build precise control graphs for binary code. We demonstrate on a set of benchmarks that our technique can consistently construct precise CFGs for binary code.