GitHub - bacam/coqjvm: Coq executable semantics and resource verifierThis repository contains: An executable semantics for a substantial fragment of the JVM in Coq [1]; a verifier for simple resource properties where the specifications and proofs are embedded in class files, written in Coq; an OCaml library for dealing with JVM classfiles; and a slightly modified copy of extlib 1.5 (see below). At the time of writing, I was able to build it with OCaml 4.02.3 and Co
https://dl.acm.org/citation.cfm?id=1786136
