Bi-abductive Resource Invariant Synthesis

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.

• Type: Conference
• Year: 2009
• Where: APLAS
• Authors: Cristiano Calcagno, Dino Distefano, Viktor Vafeiadis
• Keywords: Algorithm, APLAS 2009, Concurrent Programs, Programming Languages, Resource Invariants