Functional verification of asynchronous systems and protocols

Asynchronous message-passing systems are employed frequently to implement distributed mechanisms, protocols, and processes. This work addresses the problem of verification of properties of such systems by static analysis. The key feature of our approach is to increase precision by eliding a large subset of infeasible execution paths within the system, which are paths along which more messages are received than the number of messages sent so far in the path.  We have implemented our approach, and have analyzed its performance on a set of 14 benchmarks. On these benchmarks our tool obtains significantly higher precision compared to two baseline approaches.

References:

Snigdha Athaiya, Raghavan Komondoor, and K. Narayan Kumar. “Data Flow Analysis of Asynchronous Systems using Infinite Abstract Domains”. In Proceedings of the 30th European Symposium on Programming (ESOP), 2021.