Re:Formal Verification Creates Hacker-Proof Code (2016)
by sterlind on Sunday April 26, 2020 @05:23PM
(#22990380)
exactly. I've proven that in a scenario with a certain number of zones and workers, the invariants and temporal properties cannot be violated.
With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)
With more work, I could prove the invariants for any number of workers and zones using TLAPS rather than TLC, though I couldn't prove the temporal properties in this way (since TLAPS doesn't support temporal logic, it can only prove invariants.)