utwente-fmt / vercors

The VerCors verification toolset for verifying parallel and concurrent software

https://utwente.nl/vercors

Mozilla Public License 2.0

58 stars 26 forks source link

VeyMont: lightweight permissions #1244

Closed bobismijnnaam closed 2 months ago

bobismijnnaam commented 2 months ago

Checklist:

[ ] The wiki is updated in accordance with the changes in this PR. For example: syntax changes, semantics changes, VerCors flags changes, etc.

PR description

This PR implements a more lightweight model of stratified permission which simplifies the implementation, allows proper functioning of \chor without ad-hoc hacks, and hopefully speeds up verification.