Formal-Methods

Symptom SAT is NP-complete (T027). It is the NP-complete problem, the one everything else reduces to. The textbook conclusion is that you should avoid it. Meanwhile: a hardware verification team routinely discharges instances with two million variables and ten million clauses in under a minute. Package managers solve dependency resolution with SAT. Every bounded model checker (T049) is a SAT solver with a front end. The planning community abandoned custom search for SAT encodings and got faster. ...

Symptom Your distributed lock service deadlocks once a month. You cannot reproduce it. The logs show three nodes in states that, as far as you can reconstruct, should not co-occur. You add tracing. It does not happen again for six weeks, then happens twice in a day during a deploy. You write a stress test that runs a million random interleavings overnight and finds nothing. ...

Symptom You changed a loop. It looks right. The tests pass. You are not confident. The reason you are not confident is that the tests check a finite set of inputs and the loop runs on all of them. You know this. So you stare at the loop and try to convince yourself by simulating it in your head, which works for three iterations and then stops working. ...

Symptom Rice’s theorem (T011) told you every non-trivial semantic property is undecidable. Your static analyzer must therefore be unsound, incomplete, or non-terminating. In practice it is incomplete: it reports things that cannot happen. ...

Symptom “Well-typed programs don’t go wrong.” You have heard it. You have probably said it. And then: String s = null; s.length(); // NullPointerException That program is well typed and it went wrong. So either the slogan is false or it means something narrower than it sounds. It means something narrower, and the narrowness is precisely specifiable. ...