7 ms·

Does this use tactics to identify contradictions, tautologies, subsumptions, etc in conditions? How does this work?

• yaantc 4y ago
  A static analyzer does what is called "abstract interpretation". A good introduction on the principles is [1], from pioneers in the field. Very briefly, the analysis tries to approximate the "states space" for the program, and if it intersect problematic value then it detects a bug. For example, if it can approximate the range of values a variable "x" can take, and this range includes 0 and x is used for division, then a division by zero bug can happen. When an issue is found, those tools can give you the detailed path leading to the bug, from input down to a call chain to the bug. The challenge here is to find a good approximation of the possible states. If the tool over-approximate, there will be false alarms. If it under approximate, it will miss bugs. Most tools do a bit of both ;) [1] https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html https://www.di.ens.fr/~cousot/AI/IntroAbsInt.html
  • goombacloud 4y ago
    Not all static analyzers use abstract interpretation (they should though to find all issues) because they may implement a rules based approach of checking against "common" bugs, or they may use model checking, or they may use some other form of symbolic execution, or do concolic execution.
    • aziem 4y ago
      I think Patrick Cousot (and others) would argue that most of those are some form of abstract interpretation :)