Proving correctness of compiler optimizations by temporal logic. - David Lacey; Neil D. Jones; Eric Van Wyk; Carl Christian Frederiksen (POPL, 2002)

Correctness of Classical Compiler Optimizations using CTL. - Carl Christian Frederiksen (COCV@ETAPS, 2002)

Compiler Optimization Correctness by Temporal Logic. - David Lacey; Neil D. Jones; Eric Van Wyk; Carl Christian Frederiksen (High. Order Symb. Comput., 2004)

Sub-Computation Based Transition Predicate Abstraction. - Carl Christian Frederiksen; Masami Hagiya (Inf. Media Technol., 2007)