zbMATH — the first resource for mathematics

Transactions for software model checking. (English) Zbl 1271.68086
Dawar, Anuj (ed.), SoftMC 2003. Workshop on software model checking (satellite workshop of CAV ’03), Ottawa, Canada, June 26–27, 2003. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 89, No. 3, 518-539 (2003).
Summary: This paper presents a software model checking algorithm that combats state explosion by decomposing each thread’s execution into a sequence of transactions that execute atomically. Our algorithm infers transactions using the theory of reduction, and supports both left and right movers, thus yielding larger transactions and fewer context switches than previous methods. Our approach uses access predicates to support a wide variety of synchronization mechanisms. In addition, we automatically infer these predicates for programs that use lock-based synchronization.
For the entire collection see [Zbl 1271.68030].

68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: Link