Modular Verification with Shared Abstractions

In: International Workshop on Foundations of Object-Oriented Languages (FOOL'09). 2008

Authors

• Uri Juhasz
• Noam Rinetzky
• Arnd Poetzsch-Heffter
• Mooly Sagiv
• 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.

Full Text

• PDF: mvsa.pdf
• PS.GZ: mvsa.ps.gz

BibTeX

@InProceedings{Juhasz.Rinetzky.EA08modular, 
   author = {Uri Juhasz and Noam Rinetzky and Arnd Poetzsch-Heffter and Mooly Sagiv and Eran Yahav}
   title = {Modular Verification with Shared Abstractions},
   booktitle = {International Workshop on Foundations of Object-Oriented Languages (FOOL'09)},
   year = {2008},
}