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