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.
Path to example file
Lines of code
57 lines (comments not included)
Lines of specification
20 lines (35.09% of the total)
Note, verification may take a while and has a time-out of 20 seconds.