. "Hol\u00EDk, Luk\u00E1\u0161" . . . . "19th International Conference, TACAS 2013" . . . "Abdulla, Parosh" . "15"^^ . . "[435CAF486D4B]" . . "60384" . . . "An Integrated Specification and Verification Technique for Highly Concurrent Data Structures"@en . "Jonsson, Bengt" . . "An Integrated Specification and Verification Technique for Highly Concurrent Data Structures" . . . . "Berlin Heidelberg" . "An Integrated Specification and Verification Technique for Highly Concurrent Data Structures" . . "Haziza, Fr\u00E9d\u00E9ric" . . "1"^^ . . . "RIV/00216305:26230/13:PU106304" . "2013-03-18+01:00"^^ . . "\u0158\u00EDm" . "978-3-642-36742-7" . . "verification, specification, concurrency, parallelism, lock-free data structures, automata, data independence, thread modular, precision"@en . "26230" . . "P(GAP103/10/0306)" . "We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations bet"@en . "5"^^ . "Springer-Verlag" . . . "Rezine, Ahmed" . "An Integrated Specification and Verification Technique for Highly Concurrent Data Structures"@en . "RIV/00216305:26230/13:PU106304!RIV14-GA0-26230___" . "We present a technique for automatically verifying safety properties of concurrent programs, in particular programs which rely on subtle dependencies of local states of different threads, such as lock-free implementations of stacks and queues in an environment without garbage collection. Our technique addresses the joint challenges of infinite-state specifications, an unbounded number of threads, and an unbounded heap managed by explicit memory allocation. Our technique builds on the automata-theoretic approach to model checking, in which a specification is given by an automaton that observes the execution of a program and accepts executions that violate the intended specification. We extend this approach by allowing specifications to be given by a class of infinite-state automata. We show how such automata can be used to specify queues, stacks, and other data structures, by extending a data-independence argument. For verification, we develop a shape analysis, which tracks correlations bet" .