Formalization of the Habanero-Java programming model. We focus primarily on the formalization of safety properties, such as deadlock freedom and race freedom. The overarching goal of the project is to provide theoretical framework, read a Coq library, for the verification of synchronization mechanisms.
[PLACES'16] Formalization of Phase Ordering
We are currently working on:
- deadlock-free subset of phaser operations
- async-finish
We use OPAM and Coq Shell for the development.
This project depends on Aniceto, so you need to install it first:
git clone https://bitbucket.org/cogumbreiro/aniceto-coq
To setup the requirements of this software do:
source configure.sh # to install dependencies and setup the environment
To setup CoqIDE in MacOS you need to set the path of coqtop to be aware
of your OPAM installation.
Navigate to CoqIDE -> Externals -> coqtop and set the output of the
following command:
which coqtop