Calcagno, Cristiano; Parkinson, Matthew; Vafeiadis, Viktor Modular safety checking for fine-grained concurrency. (English) Zbl 1211.68082 Nielson, Hanne Riis (ed.) et al., Static analysis. 14th international symposium, SAS 2007, Kongens Lyngby, Denmark, August 22–24, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-74060-5/pbk). Lecture Notes in Computer Science 4634, 233-248 (2007). Summary: Concurrent programs are difficult to verify because the proof must consider the interactions between the threads. Fine-grained concurrency and heap allocated data structures exacerbate this problem, because threads interfere more often and in richer ways. In this paper we provide a thread-modular safety checker for a class of pointer-manipulating fine-grained concurrent algorithms. Our checker uses ownership to avoid interference whenever possible, and rely/guarantee (assume/guarantee) to deal with interference when it genuinely exists.For the entire collection see [Zbl 1123.68008]. Cited in 19 Documents MSC: 68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) 68Q60 Specification and verification (program logics, model checking, etc.) Software:ESC/Java; Spec#; Zing PDFBibTeX XMLCite \textit{C. Calcagno} et al., Lect. Notes Comput. Sci. 4634, 233--248 (2007; Zbl 1211.68082) Full Text: DOI