This example shows how reasoning with explicit witnesses works. It is supposed to work with Chalice, but the assertions are not proven.
|Path to example file||witnesses/predicates.pvl|
|Lines of code||50 lines (comments not included)|
|Lines of specification||25 lines (50% of the total)|
Note, verification may take a while and has a time-out of 20 seconds.