Log-based set in VeriFast (partial)

· Uncategorized
Author

logset

 

Very partial.

Defined an abstraction relation.

Defined a rely condition.

Verified major part of update(). Did not verify lookup() or collect() or advance of tl, but invariant/rely condition should allow their verification. Will continue with this proof now.

1 Comment

Comments RSS

Leave a Comment