To Goto Where No Statement Has Gone Before

This paper presents a method for deriving an expression from the low-level code compiled from an expression in a high-level language. The input is a low-level control flow graph (CFG) and the derived expression is in a form that can be used as input to an automatic theorem prover. The method is useful for program verification systems that take as input both programs and specifications after they have been compiled from a high-level language. This is the case for systems that encode specifications in an existing programming language and do not have a special compiler. The method always produces an expression, unlike the heuristics for decompilation which may fail. It is efficient: the resulting expression is linear in the size of the CFG by maintaining all sharing of subgraphs.