4 ms·
How very interesting. Does that detect issues at runtime, or prove statically that the code is "safe" (whatever the remit of that definition is here)? If the
by rich_sasha 2y ago
How very interesting.
Does that detect issues at runtime, or prove statically that the code is "safe" (whatever the remit of that definition is here)?
If the former, I guess you're still at the mercy of test coverage and all the pitfalls it entails.
- nanolith 2y agoModel checking employs abstract interpretation, so it's similar to static analysis. I hesitate to use the latter term, because it's often used to describe how linting works. This is significantly more advanced. The model checker translates an abstract model of execution for the code into an SMT solver, and uses this to find counter-examples. The SMT solver works backward from failure cases to discover a combination of inputs or program state that can cause any one of these failure cases. This traces memory, data flow, and control flow. It's actually a pretty neat thing. It doesn't require existing test coverage or anything at runtime to work.