Linked list properties

In this verification problem several properties of linked lists are verified. This is done via abstraction to sequences and asserting certain properties over these sequences.

General information

ID95
Articlenone
Back-endSilicon
LanguagePVL
FeaturesLists, Sequences
Sources
Path to example filemanual/list.pvl
Date2017-06-20

Statistical information

Lines of code30 lines (comments not included)
Lines of specification11 lines (36.67% of the total)
Computation time16674 milliseconds

Example code

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