History-based Verification of Functional Behaviour of Concurrent Programs

Stefan Blom, Marieke Huisman, M. Zaharieva

  • 6 Citations

Abstract

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.
Original languageUndefined
Place of PublicationEnschede
PublisherCentre for Telematics and Information Technology (CTIT)
Number of pages25
StatePublished - 9 Mar 2015

Publication series

NameCTIT Technical Report Series
PublisherUniversity of Twente, Centre for Telematics and Information Technology (CTIT)
No.TR-CTIT-15-02
ISSN (Print)1381-3625

Fingerprint

Algebra
Specifications

Keywords

  • METIS-312523
  • EWI-25866
  • concurrent programsmodular verificationbehavioural specifications
  • behavioural specifications
  • IR-95383
  • Concurrent programs
  • Modular Verification

Cite this

Blom, S., Huisman, M., & Zaharieva, M. (2015). History-based Verification of Functional Behaviour of Concurrent Programs. (CTIT Technical Report Series; No. TR-CTIT-15-02). Enschede: Centre for Telematics and Information Technology (CTIT).

Blom, Stefan; Huisman, Marieke; Zaharieva, M. / History-based Verification of Functional Behaviour of Concurrent Programs.

Enschede : Centre for Telematics and Information Technology (CTIT), 2015. 25 p. (CTIT Technical Report Series; No. TR-CTIT-15-02).

Research output: ProfessionalReport

@book{b94ea049bd7149acb7a0cdb62202fe6a,
title = "History-based Verification of Functional Behaviour of Concurrent Programs",
abstract = "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.",
keywords = "METIS-312523, EWI-25866, concurrent programsmodular verificationbehavioural specifications, behavioural specifications, IR-95383, Concurrent programs, Modular Verification",
author = "Stefan Blom and Marieke Huisman and M. Zaharieva",
year = "2015",
month = "3",
series = "CTIT Technical Report Series",
publisher = "Centre for Telematics and Information Technology (CTIT)",
number = "TR-CTIT-15-02",
address = "Netherlands",

}

Blom, S, Huisman, M & Zaharieva, M 2015, History-based Verification of Functional Behaviour of Concurrent Programs. CTIT Technical Report Series, no. TR-CTIT-15-02, Centre for Telematics and Information Technology (CTIT), Enschede.

History-based Verification of Functional Behaviour of Concurrent Programs. / Blom, Stefan; Huisman, Marieke; Zaharieva, M.

Enschede : Centre for Telematics and Information Technology (CTIT), 2015. 25 p. (CTIT Technical Report Series; No. TR-CTIT-15-02).

Research output: ProfessionalReport

TY - BOOK

T1 - History-based Verification of Functional Behaviour of Concurrent Programs

AU - Blom,Stefan

AU - Huisman,Marieke

AU - Zaharieva,M.

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 - METIS-312523

KW - EWI-25866

KW - concurrent programsmodular verificationbehavioural specifications

KW - behavioural specifications

KW - IR-95383

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)

ER -

Blom S, Huisman M, Zaharieva M. History-based Verification of Functional Behaviour of Concurrent Programs. Enschede: Centre for Telematics and Information Technology (CTIT), 2015. 25 p. (CTIT Technical Report Series; TR-CTIT-15-02).