Proof-producing synthesis from logic
I firmly believe that generating code that is correct-by-construction is a more effective technique for producing verified code than traditional post-hoc verification techniques. In exploring this, I've developed various proof-producing synthesis tools which generate, from specifications in higher-order logic, machine code, ML or hardware that is guaranteed to adhere to the given specification.
Reversing decompilation: synthesis of machine code
Given an implementation of decompilation, it is very easy to produce a translation-validation-based tool that essentially reverses the decompiler (CC'09). Given some tail-recursive functions, the tool produces machine code that is guaranteed (by a certificate theorem) to implement the given functional specification. The beauty of the details of this approach is the support for user-defined extensions by teaching the compiler about a domain-specific language.
Synthesis of ML from HOL
In the theorem proving community, it has become commonplace to define functions in the logic of the prover, prove correctness properties of these functions and then invoke a code generation mechanism within the prover which prints the logic function in the syntax of real functional programming language (such as Haskell, ML, Ocaml or Scala). In a paper at ICFP'12, Scott Owens and I show how these code generators can be made proof producing and hence more trustworthy.
Bluespec-inspired synthesis of hardware from HOL
Recently, I have been experimenting with synthesis of hardware from HOL using ideas from the Bluespec tool-chain and advice from David Greaves. The aim of this is to learn about hardware and to provide an alternative to a different technique for synthesising hardware from HOL by Mike Gordon et al. A target case study, we have in mind, is to produce a verified processor that can run output from an ML compiler that Ramana Kumar is developing.