We have applied the Observation Sequence paradigm to the undecidable problem of analyzing reachability for concurrent procedures communicating via global-scope variables PLDI 2018. Our technique is dubbed CUBA (Context-UnBounded Analysis).
We have also applied this paradigm to unbounded-queue message passing systems written in the P language, such as distributed communication protocols CAV 2019. Our technique is dubbed QUBA (Queue-UnBounded Analysis).
Please refer to the left for more details on applications.