Reasoning about Java programs higher order logic using PVS and Isabelle by M. Huisman