PCC

A light-weight approach for certification of monitor inlining for sequential Java bytecode using proof-carrying code, formalized in Coq.

Meta

• Author(s):
  • Andreas Lundblad (initial)
  • Karl Palmskog
• License: MIT License
• Compatible Coq versions: 8.10 or later
• Additional dependencies: none
• Coq namespace: PCC
• Related publication(s):
  • A Proof Carrying Code Framework for Inlined Reference Monitors in Java Bytecode

Building instructions

git clone https://github.com/palmskog/pcc.git
cd pcc
make   # or make -j <number-of-cores-on-your-machine>

Documentation

The paper has more information about the approach.