[cocci] Applying symbolic evaluation/execution together with computation tree logic variants?

[Markus Elfring <Markus.Elfring@web.de>]

Hello,

Source code search approaches (also based on the semantic patch language)
try to detect patterns for improvable implementation details.

* Such searches can specify (by SmPL ellipses for example) that code parts
  should be treated as “unknown”.
  But the corresponding code places can also contain valuable information.

* Search patterns tend to combine items from multiple places.
  Thus limited knowledge is extracted and reused.


I got the impression that some data processing approaches are needed
where higher level properties should be determined from complete implementation details.
It seems that symbolic evaluation/execution is used for this purpose.

Would you find a document (like the following) interesting for further
development considerations accordingly?

Petri Net Based Symbolic Model Checking for Computation Tree Logic of Knowledge
by Guanjun Liu and Leifeng He
https://doi.org/10.48550/arXiv.2012.10126

Regards,
Markus