imho, model checker suits for the problem with many different states and complex state transformation.
But in this case, it's a simple toctou problem.. Using model checker sounds weird for me
Yeah, I was going to say, if anybody with distributed systems knowledge actually thought about this code, it wouldn't have happened.
If you added model checking to it you could have prevented it though, because people that know how to program a model checking program, will see the error right away.
Comments
imho, model checker suits for the problem with many different states and complex state transformation. But in this case, it's a simple toctou problem.. Using model checker sounds weird for me
Yeah, I was going to say, if anybody with distributed systems knowledge actually thought about this code, it wouldn't have happened.
If you added model checking to it you could have prevented it though, because people that know how to program a model checking program, will see the error right away.