CoJaq is a platform for formalisation of the Java Virtual Machine features. It contains a hierarchical formalisation of the Java bytecode language mechanised in Coq proof assistant. It can be used for several pruposes, including:
CoJaq can be compiled and used in Coq v.8.4.
People who develop CoJaq are:
If you want to contact us, please email to: . Especially, when you discover a bug.