Modular Verification with Shared Abstractions

Uri Juhasz, Noam Rinetzky, Arnd Poetzsch-Heffter, Mooly Sagiv and Eran Yahav


Modular verification of shared data structures is a challenging problem: Side-effects in one module that are observable in another module make it hard to analyze each module separately. We present a novel approach for modular verification of shared data structures. Our main idea is to verify that the inter-module sharing is restricted to a user-provided specification which also enables the analysis to handle side-effects.

Full paper


Presented at FOOL'09; Saturday, 24 January 2009, Savannah, Georgia, USA.