3 ms·

If you have not used a model checker you don't have a proof. Please don't say that you have one. You are just hoping for the best. See this to get yourself sta

If you have not used a model checker you don't have a proof. Please don't say that you have one. You are just hoping for the best. See this to get yourself started: http://research.microsoft.com/en-us/um/people/lamport/tla/byzpaxos.html http://research.microsoft.com/en-us/um/people/lamport/tla/by...

deleted 12y ago
[deleted]
aurelius 12y ago
If you have used a model checker, you probably don't have a proof either. You have a model that might not be accurate, and testing all its inputs may be combinatorially prohibitive.
- sseveran 12y ago
  thats not the real issue. The issue with model checkers is verifying that production code actually exactly implements the model.
  - aurelius 12y ago
    Yes, that is <i>another</i> issue with model checkers. Either way, your original comment is still nonsense.
    - sseveran 12y ago
      No. No it is not. See the Amazon paper if you want an overview.