Overview

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.

Download

Documentation

Contact

People who develop CoJaq are:

If you want to contact us, please email to: email. Especially, when you discover a bug.


Valid HTML 4.01! Valid CSS!