Please use this identifier to cite or link to this item:
Title: The use of model-checking for the verification of concurrent algorithms
Authors: Cordina, Joseph
Keywords: Computer algorithms
Computer programs -- Verification
Computer programs -- Correctness
Issue Date: 2004
Publisher: University of Malta. Faculty of ICT
Citation: Cordina, J. (2004). The use of model-checking for the verification of concurrent algorithms. 2nd Computer Science Annual Workshop (CSAW’04), Kalkara. 29-35.
Abstract: The design of concurrent algorithms tends to be a long and difficult process. Increasing the number of concurrent entities to realistic numbers makes manual verification of these algorithms almost impossible. Designers normally resort to running these algorithms exhaustively yet can never be guaranteed of their correctness. In this report, we propose the use of a model-checker (SMV) as a machine-automated tool for the verification of these algorithms. We present methods how this tool can be used to encode algorithms and allow properties to be guaranteed for uni-processor machines running a scheduler or SMP machines. We also present a language-generator allowing the designer to use a description language that is then automatically converted to the model-checker’s native language. We show how this approach was successful in encoding a concurrent algorithm and is able to verify the desired properties.
Appears in Collections:Scholarly Works - FacICTCS

Files in This Item:
File Description SizeFormat 
Proceedings of CSAW’04 - A3.pdf122.61 kBAdobe PDFView/Open

Items in OAR@UM are protected by copyright, with all rights reserved, unless otherwise indicated.