Simple model abstraction

Very simple verification example with model-based abstraction. A process algebraic model is created that is able to perform a single action: "step", which increments some shared variable by one. We verify that this is a valid abstraction of a program that increases some shared value by one.

General information

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

Statistical information

Lines of code57 lines (comments not included)
Lines of specification20 lines (35.09% of the total)
Computation time24786 milliseconds

Example code

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