Machine-code verification for multiple architectures: an application of decompilation into logic

Portland, OR, 2008, Pages 1-8E.

Cited by: 48|Bibtex|Views5|Links
EI WOS
Keywords:
machine codedifferent machine languagemachine-code verificationhol4 systemdetailed modelMore(19+)

Abstract:

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

Code:

Data:

Your rating :
0

 

Tags
Comments