Model Checking Unbounded Concurrent Lists

Autor:	Sharad Malik, Muralidhar Talupur, Divjyot Sethi
Rok vydání:	2013
Předmět:	Model checking List size Concurrent data structure Programming language Computer science Bounded function computer.software_genre Data structure computer Abstraction (linguistics)
Zdroj:	Model Checking Software ISBN: 9783642391750 SPIN
DOI:	10.1007/978-3-642-39176-7_20
Popis:	We present a model checking based method for verifying list-based concurrent data structures. Concurrent data structures are notorious for being hard to get right and thus, their verification has received significant attention from the verification community. These data structures are unbounded in two dimensions: the list size is unbounded and an unbounded number of threads access them. Thus, their model checking requires abstraction to a model bounded in both the dimensions.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::0ac170fe857e2cd10b42d0ed9eecc736 https://doi.org/10.1007/978-3-642-39176-7_20 Zobrazit plný text záznamu