tr-announce April 2007

tr-announce@lists.rwth-aachen.de

1 participants
1 discussions

2007-6: Verifying Concurrent List-Manipulating Programs by LTL Model Checking

by Peter Schneider-Kamp

The following technical report is available from http://aib.informatik.rwth-aachen.de: Verifying Concurrent List-Manipulating Programs by LTL Model Checking Joost-Pieter Katoen, Thomas Noll, and Stefan Rieger AIB 2007-06 We present a novel approach to the verification of concurrent pointer-manipulating programs which operate on singly-linked lists. By abstracting from chains (i.e., non-interrupted sublists) in the heap, we obtain a finite-state representation of all possible executions of a given program. The combination of a simple pointer logic for expressing heap properties and of temporal operators then allows us to employ standard LTL model checking techniques. The usability of this approach is demonstrated by establishing correctness properties of a producer/consumer system and of a concurrent garbage collector.

17 years, 4 months

2024

2023

2022

2021

2020

2019

2018

2017

2016

2015

2014

2013

2012

2011

2010

2009

2008

2007

2006

2005

2004

2003

2002

2001

tr-announce April 2007