Re:Writing correct lock-free and distributed stateful system...
by nickpsecurity on Friday May 19, 2017 @12:10PM
(#14377041)
No, I meant implementation in SPARK. The specs were already done in TLA+ in the OP's model. There's also implied porting between two notations.
[ Parent
| on HN ]
There are no comments on this comment yet.