For processing compiled code, model checkers require accurate model extraction from binaries. We present our fully configurable
binary analysis platform Jakstab, which resolves indirect branches by multiple rounds of disassembly interleaved with dataflow analysis. We demonstrate that
this iterative disassembling strategy achieves better results than the state-of-the-art tool IDA Pro.
Supported by DFG grant FORTAS – Formal Timing Analysis Suite for Real Time Programs (VE 455/1-1) and the European Commission
under Contract IST-2002-507932 ECRYPT.