A formal definition of JML in Coq and its application to runtime assertion checking

Hermann Lehner. A formal definition of JML in Coq and its application to runtime assertion checking. PhD thesis, ETH Zurich, Zürich, Switzerland, 2011. [doi]

Abstract

Abstract is missing.