Modular Verification with Shared Abstractions
Uri Juhasz, Noam Rinetzky, Arnd Poetzsch-Heffter,
Mooly Sagiv and Eran Yahav
Abstract
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.
Presented at FOOL'09; Saturday, 24 January
2009, Savannah, Georgia, USA.