In einer Welt in der Sicherheitslücken in Software eine latente Bedrohung der vernetzten Gesellschaft darstellt, wird die Analyse von fremder Software, in der Form von ausführbaren Programmen, immer wichtiger. Während die Verifikation von Quellcode in den letzten Jahrzehnten viel Aufmerksamkeit auf sich gezogen hat, ist das Ziel dieser Arbeit eine Infrastruktur für korrekte Analysen von Binärdateien bereitzustellen, um dadurch das Verstehen und die Verifikation von ausführbaren Programmen zu ermöglichen.     «

In einer Welt in der Sicherheitslücken in Software eine latente Bedrohung der vernetzten Gesellschaft darstellt, wird die Analyse von fremder Software, in der Form von ausführbaren Programmen, immer wichtiger. Während die Verifikation von Quellcode in den letzten Jahrzehnten viel Aufmerksamkeit auf sich gezogen hat, ist das Ziel dieser Arbeit eine Infrastruktur für korrekte Analysen von Binärdateien bereitzustellen, um dadurch das Verstehen und die Verifikation von ausführbaren Programmen zu erm...     »