Traffic is a well-established, well-formed model, which uses symbols heavily in order to mazimize our safety and to optimize the traffic flow.


Each traffic light signals about the corresponding crossing, road, lane or other critical part of traffic.  Traffic lights are controlled either based on time intervals or using detectors, traffic sensors. We make interpretations based on the present color of the symbol.

Our behavior is controlled by the logic: for green we can drive, for red we must wait. In order to get further we ask from ourselves: can we go further, or must we wait. This query/answering-process is natural and characteristic for all of us, because by using this mechanism we get pragmatic value: we reach home or work or hobby or any place.

Source code analysis

It is obvious that in source code analysis we use similar principles as in traffic (above). However, the symbols are different and the logic varies very much from the one, learnt for traffic. Still, if we formulate a source code model navigation process as a map or a topology, which resembles traffic, we can find same kind of formalisms in both areas. This is the main topic of this blog.

Symbolic Program Analysis

Symbolic program analsysis (SPA) is a metatheory to make necessary model transformations from an atomistic source code model in order to detect possible contradictions. All metatheories inherit tautology (See Sowa).


There are specific program analyses like the ones for loops, data, object behavior, mastering side effects as well as user defined approaches in order to make a free mix.