-
- Downloads
Bump Iris, use the new feature of iStartProof, and do many simplifications in singlewriter.v.
Showing
- theories/escrows.v 1 addition, 1 deletiontheories/escrows.v
- theories/examples/kvnode.v 24 additions, 35 deletionstheories/examples/kvnode.v
- theories/examples/ticket_lock.v 4 additions, 12 deletionstheories/examples/ticket_lock.v
- theories/fork.v 1 addition, 2 deletionstheories/fork.v
- theories/fractor.v 28 additions, 2 deletionstheories/fractor.v
- theories/gps/fractional.v 7 additions, 14 deletionstheories/gps/fractional.v
- theories/gps/plain.v 5 additions, 10 deletionstheories/gps/plain.v
- theories/gps/shared.v 9 additions, 10 deletionstheories/gps/shared.v
- theories/gps/singlewriter.v 302 additions, 437 deletionstheories/gps/singlewriter.v
- theories/invariants.v 4 additions, 6 deletionstheories/invariants.v
- theories/lifting_vProp.v 1 addition, 1 deletiontheories/lifting_vProp.v
- theories/malloc.v 5 additions, 7 deletionstheories/malloc.v
- theories/na.v 12 additions, 17 deletionstheories/na.v
- theories/persistor.v 16 additions, 11 deletionstheories/persistor.v
- theories/weakestpre.v 5 additions, 6 deletionstheories/weakestpre.v
- theories/wp_tactics_vProp.v 1 addition, 2 deletionstheories/wp_tactics_vProp.v
Loading
Please register or sign in to comment