Bytecode Model Checking: An Experimental Analysis. - David A. Basin; Stefan Friedrich 001; Marek Gawkowski; Joachim Posegga (SPIN, 2002)

Verified Bytecode Model Checkers. - David A. Basin; Stefan Friedrich 001; Marek Gawkowski (TPHOLs, 2002)

Bytecode Verification by Model Checking. - David A. Basin; Stefan Friedrich 001; Marek Gawkowski (J. Autom. Reason., 2003)

Towards Proof Generating Compilers. - Arnd Poetzsch-Heffter; Marek Gawkowski (COCV@ETAPS, 2004)

Formal framework for proof generating optimizers. - Marek Gawkowski (2008)