Transactions for Software Model Checking
- Shaz Qadeer
Proceedings of the Workshop on Software Model Checking (published as volume 89 of Electronic Notes in Theoretical Computer Science) |
Published by Elsevier
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