TY - BOOK
T1 - History-based Verification of Functional Behaviour of Concurrent Programs
AU - Blom, Stefan
AU - Huisman, Marieke
AU - Zaharieva-Stojanovski, Marina
PY - 2015/3/9
Y1 - 2015/3/9
N2 - Modular verification of the functional behaviour of a concurrent program remains a challenge. We propose a new way to achieve this, using histories, modelled as process algebra terms, to keep track of local changes. When threads terminate or synchronise in some other way, local histories are combined into global histories, and by resolving the global histories, the reachable state properties can be determined. Our logic is an extension of permission-based separation logic, which supports expressive and intuitive specifications. We discuss soundness of the approach, and illustrate it on several examples.
AB - Modular verification of the functional behaviour of a concurrent program remains a challenge. We propose a new way to achieve this, using histories, modelled as process algebra terms, to keep track of local changes. When threads terminate or synchronise in some other way, local histories are combined into global histories, and by resolving the global histories, the reachable state properties can be determined. Our logic is an extension of permission-based separation logic, which supports expressive and intuitive specifications. We discuss soundness of the approach, and illustrate it on several examples.
KW - Concurrent programsmodular verificationbehavioural specifications
KW - Behavioural specifications
KW - Concurrent programs
KW - Modular Verification
M3 - Report
T3 - CTIT Technical Report Series
BT - History-based Verification of Functional Behaviour of Concurrent Programs
PB - Centre for Telematics and Information Technology (CTIT)
CY - Enschede
ER -