Adaptable Static Analysis of Executables for proving the Absence of Vulnerabilities

摘要: In a world where vulnerabilities in software pose an inherent threat for the networked society, analyzing third-party software, form of executable programs, becomes increasingly important. While program verification at source code level has received much attention last decades, this thesis focuses on providing sound and precise analysis framework binaries, thereby enabling understanding, auditing, programs.