We describe a parallel, symbolic, model-checking algorithm, built around a compositional reasoning method. The method constructs a collection of per-process (i.e., local) invariants, which together imply a desired global safety property. The local invariant computation is a simultaneous fixpoint evaluation, which easily lends itself to parallelization. Moreover, locality of reasoning helps limit both the frequency and the amount of cross-thread synchronization, leading to good parallel performance. Experimental results show that the parallelized computation can achieve substantial speed-up, with reasonably small memory overhead. © 2011 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Cohen, A., Namjoshi, K. S., Sa’Ar, Y., Zuck, L. D., & Kisyova, K. I. (2011). Parallelizing a symbolic compositional model-checking algorithm. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6504 LNCS, pp. 46–59). https://doi.org/10.1007/978-3-642-19583-9_9
Mendeley helps you to discover research relevant for your work.