Search code examples
testingstatic-analysisverificationsymbolic-execution

error detection in static analysis and symbolic execution


what kind of errors static analysis (e.g. compiler) can detect and symbolic execution can not detect? and what kind of errors that symbolic execution can detect and static analysis can not detect? for example can symbolic execution detect syntax errors?


Solution

  • In short, static analysis is capable of spotting coding issues, such as bad practices. For example, if you declare (unnecessarily) a class field as public, a static analysis tool may warn you that such field should be declared as private. However, the "cleanest" code is not necessarily bug free. Although, no malpractices can be found in some code, an incorrect reasoning on behalf of the coder may lead (later) to a crash in runtime.

    For example, if we develop clean code to implement a calculator, then a static analysis tool does not output any warning, however if we forget to verify the input to prevent the user from attempting a division by zero, then the our calculator would eventually crash in runtime.

    On the other hand, Symbolic (or Concolic) execution executes the target program, hence they have the potential to achieve any possible runtime execution state of the program, such as inducing a runtime error caused by a bug. In the above-described calculator example, symbolic execution would find the runtime failure and would also tell us which inputs induce such failure. To answer your last question, symbolic execution is not meant to inspect the quality of the code.

    Ideally, we should use both before releasing the software.