• Contrast Style 4
  • Contrast Style 3
  • Contrast Style 2
  • Contrast Style 1
Text size

Logics and analyses for concurrent heap-manipulating programs

Alexey Gotsman (author)

UK Price: £75.00 EU Price: €95.00 ROW (USD) Price: $105.00 
add to basket

Buy this eBook

BCS eBooks are available in a variety of formats, including Kindle, ePub and PDF. You can purchase this title from a number of online retailers (including those listed below).

ISBN: 9781906124830
Format: Paperback
Dimensions: 210 x 297 x 8.814
Number of pages: 162
Publication date: 14 MAR 2011
Publisher: BCS, The Chartered Institute for IT

Reasoning about concurrent programs is difficult because of the need to consider all possible interactions between concurrently executing threads. The problem is especially acute for programs that manipulate shared heap-allocated data structures, since heap-manipulation provides more ways for threads to interact. Modular reasoning techniques sidestep this difficulty by considering every thread in isolation under some assumptions on its environment. In this dissertation the author develops modular program logics and program analyses for the verification of concurrent heap-manipulating programs. The approach is to exploit reasoning principles provided by program logics to construct modular program analyses and to use this process to obtain further insights into the logics. In particular, the author builds on concurrent separation logic—a Hoare-style logic that allows modular manual reasoning about concurrent programs written in a simple heap-manipulating programming language. The contributions are twofold. First, it shows the soundness of concurrent separation logic without the conjunction rule and the restriction that resource invariants be precise, and to construct an analysis for concurrent heap-manipulating programs that exploit this modified reasoning principle to achieve modularity. Secondly, it develop logics and analyses for modular reasoning about features present in modern languages and libraries for concurrent programming: storable locks, first-order procedures and dynamically-created threads.
Alexey Gotsman is an assistant research professor at the IMDEA Software Institute in Madrid. He held a Postdoctoral Fellowship in Theoretical Computer Science at the University of Cambridge. His research interests are software verfication, developing reasoning techniques and automated verification tools for real-world concurrent systems software.
1 Introduction
2 Technical background
3 Static locks
4 Storable locks
5 Procedures
6 Threads
7 Conclusion

Add a review

Post a review

Reviews are subject to approval by the moderator

Your Name *

Your Email Address (Not Published) *

Your Comments *


Please type the character "x" *

* = required field