3 ms·
I do not know TLA+, but there is an abundance of other theorem provers that can model C very closely, including overflow, assignments, etc. So closely, that wh
by RaxcN 2y ago
I do not know TLA+, but there is an abundance of other theorem provers that can model C very closely, including overflow, assignments, etc.
So closely, that when you transcribe such an algorithm to C, there is very little room for error, even if the C code isn't proven directly.
- rramadass 2y ago> there is an abundance of other theorem provers that can model C very closely Can you list some/all of them please? Would be helpful to others here.