Functional Correctness Proofs of Encryption Algorithms. - Jianjun Duan; Joe Hurd; Guodong Li; Scott Owens; Konrad Slind; Junxing Zhang (LPAR, 2005)

Correctness Proofs for Device Drivers in Embedded Systems. - Jianjun Duan; John Regehr (SSV, 2010)

Formal Verification of Device Drivers in Embedded Systems. - Jianjun Duan (2013)