Is static analysis really formal verification?

Question

I have been reading about formal verification and the basic point is that it requires a formal specification and model to work with. However, many sources classify static analysis as a formal verification technique, some mention abstract intepretation and mention its use in compilers. So I am confused - how can these be formal verification if there is no formal description of the model?
EDIT: A source I found reads:

Static analysis: the abstract semantics is computed automatically from the program text according to predefined abstractions (that can sometimes be tailored automatically/manually by the user)

So does it mean it works just on the source code with no need for formal specification? This would be what static analysers do.

Also, is static analysis possible without formal verification? E.g. does SonarQube really perform formal methods?

Answer 1

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics.

How can these be formal verification if there is no formal description of the model?

A static analyser will generate control/data flow of a piece of code, upon which formal methods can then be applied to verify conformance to the system's/unit's expected design model.

Note that modelling/formal-specification is NOT a part of static-analysis.
However combined together, both of these tools are useful in formal verification.

---

For example if a system is modeled as a Finite State Machine (FSM) with

• a pre-defined number of states
  defined by a combination of specific values of certain member data.
• a pre-defined set of transitions between various states
  defined by the list of member functions.

Then the results of static analysis will help in formal verification of the fact that
the control NEVER flows along a path that is NOT present in the above FSM model.

Also, if a model can be simply defined in terms of type-definition, data-flow, control-flow/call-graph, i.e. code-metrics that a static-analyser can verify, then static-analysis itself is sufficient to formally verify that code conforms to such a model.

_{NOTE1. The yellow region above would be static analysers used to enforce stuff like coding-guidelines and naming-conventions i.e. aspects of code that cannot affect the program's behavior.}

_{NOTE2. The red region above would be formal verification that requires additional steps like 100% dynamic code-coverage, elimination of unused and dead code. These cannot be detected/enforced using a static-analyser.}

---

Static analysis is highly effective in verifying that a system/unit is implemented using a subset of the language specification to meet goals laid out in the system/unit design.

For example, if it is a design goal to prevent the stack memory from exceeding a particular limit, then one could apply a limit on the depth of recursion (or forbid recursive functions calls altogether). Static-analysis is used to identify such violations of design goals.

In the absence of any warnings from the static-analyser,
the system/unit code stands formally verified against such design-goals of its respective model.

eg. MISRA-C standard for Automotive software defines a subset of C for use in automotive systems.

MISRA-C:2012 contains

• 143 rules - each of which is checkable using static program analysis.

• 16 "directives" more open to interpretation, or relate to process.