Verifying a list iterator, implemented in Java, using witness encodings. Note that depending on which version of chalice is used, this spec may take a very very long time to check. Also, this example currently does not verify because it must be rewritten.
Lists, Loop invariants, Magic wands, Witnesses
Path to example file
Lines of code
263 lines (comments not included)
Lines of specification
162 lines (61.6% of the total)
Note, verification may take a while and has a time-out of 20 seconds.