Machine-code verification for multiple architectures: an application of decompilation into logic
Portland, OR, 2008, Pages 1-8E.
machine codedifferent machine languagemachine-code verificationhol4 systemdetailed modelMore(19+)
Realistic formal specifications of machine languages for commercial processors consist of thousands of lines of definitions. Current methods support trustworthy proofs of the correctness of programs for one such specification. However, these methods provide little or no support for reusing proofs of the same algorithm implemented in diffe...More
Full Text (Upload PDF)
PPT (Upload PPT)