Now showing items 1-1 of 1

    • Directed Proof Generation for Machine Code 

      Thakur, A.; Lim, J.; Lal, A.; Burton, A.; Driscoll, E.; Elder, M.; Andersen, T.; Reps, T. (University of Wisconsin-Madison Department of Computer Sciences, 2010)
      We present the algorithms used in McVeto (Machine-Code VErification TOol), a tool to check whether a stripped machine-code program satisfies a safety property. The verification problem that McVeto addresses is challenging ...