Forward Symbolic Execution for Trustworthy Automation of Binary Code Verification

Andreas Lindner, Karl Palmskog, Scott Constable +3

Control flow in unstructured programs can be complex and dynamic, which makes static analysis difficult. Yet, automated reasoning about unstructured control flow is important when…