Back to Search
Start Over
Safety and Liveness in Concurrent Pointer Programs.
- Source :
- Formal Methods for Components & Objects (9783540367499); 2006, p280-312, 33p
- Publication Year :
- 2006
-
Abstract
- The incorrect use of pointers is one of the most common source of software errors. Concurrency has a similar characteristic. Proving the correctness of concurrent pointer manipulating programs, let alone algorithmically, is a highly non-trivial task. This paper proposes an automated verification technique for concurrent programs that manipulate linked lists. Key issues of our approach are: automata (with fairness constraints), heap abstractions that are tailored to the program and property to be checked, first-order temporal logic, and a tableau-based model-checking algorithm. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISBNs :
- 9783540367499
- Database :
- Complementary Index
- Journal :
- Formal Methods for Components & Objects (9783540367499)
- Publication Type :
- Book
- Accession number :
- 32891715
- Full Text :
- https://doi.org/10.1007/11804192_14