University of Cambridge > > Computer Laboratory Automated Reasoning Group Lunches > Automatic Reverse Engineering for Formal Verification

Automatic Reverse Engineering for Formal Verification

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Thomas Tuerk.

This is a practice talk for HCSS with not much new material.

We describe a novel method for machine-code verification: code is decompiled into tail-recursive functions and then verification proofs are performed in the native language of a theorem prover. Unlike established methods, our completely automatic decompiler allows proof reuse even between different instruction architectures. As a case study, we have verified full functional correctness of ARM , x86 and PowerPC implementations of a version of LISP similar to LISP 1 .5. Our tools are implemented in the HOL4 system.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2023, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity