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

  Browse A-Z

Log in

University Account External (via Google)

🔐 Log In

Information on

Subscribing to talksdetails Finding a talkdetails Adding a talkdetails Disseminating talksdetails Help and Documentationdetails

ℹī¸ Information

Automatic Reverse Engineering for Formal Verification

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.

This talk is included in these lists:

Note that ex-directory lists are not shown.

Other lists

Mill Lane Lecture Rooms (Room 4), University of Cambridge, 1 Mill Lane, Cambridge CB21 Humanitarian Centre, c/o Fenner's, Gresham Rd, Cambridge CB1 2ES GN06, Computer Laboratory

Other talks

Tea and Coffee Break Shape modes of CP^1 vortices Title TBC Online Causal Inference Semina Machine Learning for Spectral Geometry and Vice Versa In conversation: Louis Herns Marcelin and Ola Osman on legacies of enslavement and contemporary violence in Liberia and Haiti
 

Š 2006-2025 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity