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:
- proving metatheoretical properties of JVML,
- proving correctness of actual bytecode programs,
- development of highly reliable code manipulation tools such as compilers, optimizers, analyzers etc.
CoJaq can be compiled and used in Coq v.8.4.
Download
- Sources and CoqDocs browsable online!
- Download sources (ZIP) (last update 2014-09-16)
- Sources of Coq files (version 0.5 - as presented in intermediate report on KKIO)
Documentation
- Representation of Java bytecode instructions in CoJaq (PDF)
- Hierarchy of CoJaq instructions
- An overview of the formalisation (PDF)
- Documentation in Coq-doc (and on-line source view)
- The initial design of the hierarchy is presented in a paper: A Dozen Instructions Make Java Bytecode, Electronic Notes in Theoretical Computer Science, Volume 264, Issue 4, 25 February 2011, Pages 19–34
Contact
People who develop CoJaq are:
If you want to contact us, please email to:
. Especially, when you discover a bug.
