Sciweavers

APLAS
2009
ACM
13 years 11 months ago
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 t...
Cristiano Calcagno, Dino Distefano, Viktor Vafeiad...
VMCAI
2009
Springer
13 years 11 months ago
Thread-Modular Shape Analysis
We present the first shape analysis for multithreaded programs that avoids the explicit enumeration of execution-interleavings. Our approach is to automatically infer a resource ...
Alexey Gotsman, Josh Berdine, Byron Cook, Mooly Sa...