Model-abstraction permissions

To establish links/simulations between programs and their abstractions, multiple kinds of points-to predicates are used. This verification example tests the behaviour of these predicates via multiple methods, some of which are failing and some succeeding.

General information

ID63
Articlenone
Back-endSilicon
LanguagePVL
FeaturesFutures
Sources
Path to example filefutures/TestFuturePerms.pvl
Date2017-06-16

Statistical information

Lines of code80 lines (comments not included)
Lines of specification29 lines (36.25% of the total)
Computation time25171 milliseconds

Example code

Note, verification may take a while and has a time-out of 20 seconds.