Decompilation into logic — verification of machine code
All software executes in the form of machine code. During my PhD, I developed a tool, a decompiler, which aids verification of machine-code programs. The tool takes machine-code programs as input and returns to the user a function describing the effect of executing the machine-code programs. The tool is proof producing: for each run, it automatically proves that the generated function is an accurate model of the behaviour of the machine code w.r.t. a specification of the operational semantics of the machine language.
The beauty of the decompiler is that the user of the tool can concentrate verification efforts on the functions the decompiler produces, since any property proved of the generated functions applies via the automatically proved certificate theorem to the original machine code.
I've used decompilation to verify functional correctness of garbage collectors and other low-level routines. The largest case study is the decompilation of the seL4 microkernel developed at NICTA. Papers on decompilation, including recent improvements to the original approach, can be found here.