Automatic Reverse Engineering for Formal Verification

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

• Magnus Myreen (University of Cambridge)
• Tuesday 12 May 2009, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

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.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.