Abstract
We describe an algorithm for synthesizing resource invariants that are used in the verification of concurrent programs. This synthesis employs bi-abductive inference to identify the footprints of different parts of the program and decide what invariant each lock protects. We demonstrate our algorithm on several small (yet intricate) examples which are out of the reach of other automatic analyses in the literature. © 2009 Springer-Verlag.
Cite
CITATION STYLE
Calcagno, C., Distefano, D., & Vafeiadis, V. (2009). Bi-abductive resource invariant synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5904 LNCS, pp. 259–274). https://doi.org/10.1007/978-3-642-10672-9_19
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
