2 ms·
>> Proving correctness is crucial in large systems. You can't do that... The model checker says the specification satisfies the properties you wrote within th
by belter 1y ago
>> Proving correctness is crucial in large systems.
You can't do that...
The model checker says the specification satisfies the properties you wrote within the finite state space you explored...
- amw-zero 1y agoYou can write proofs in TLA+ and many other formalisms. You don’t need to ever use a model checker. The proofs hold for an infinite number of infinite-length executions. We are definitely not limited to finite behaviors.