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):
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.