[tlaplus] Verifying concurrent data structures

[Jones Martins <jonesmvc@xxxxxxxxx>]

Hello, everyone

Since TLA+ can also verify (and prove) correctness of algorithms, protocols, etc., I wonder how to verify data structures. When modelling a sequential data structure compared to a concurrent data structure, how should one go about specifying it?

 For example, let's say I implemented an abstract Set specification with "Add", "Remove" and "Contains" actions. How do I prove correctness? What about a concurrent Set?

Thanks

Jones

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/667639f2-93b3-4d8d-b99f-e99dec4cbae5n%40googlegroups.com.