Enforcing Object Protocols
by Combining Static and Runtime Analysis
To run simplify proof obligations, execute the command simplify <rule>.txt
For example: simplify Boogie.txt
The test programs are structured as in table 2.
The aspects are in the directory rules.
In INVCOP package, protocols are encoded into the program.
In INVCOP++ package, protocols are separated from the program.