Abstract
Thread-modular analysis is an incomplete compositional technique for verifying concurrent systems. The heuristic works rather well when there is limited interaction among system components. In this paper, we develop a refinement algorithm that makes thread-modular model checking complete. Our algorithm refines abstract reachable states by exposing local information through auxiliary variables. The experiments show that our complete thread-modular model checking can outperform other complete compositional reasoning techniques. © 2012 Springer-Verlag.
Cite
CITATION STYLE
Meng, W., He, F., Wang, B. Y., & Liu, Q. (2012). Thread-modular model checking with iterative refinement. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7226 LNCS, pp. 237–251). https://doi.org/10.1007/978-3-642-28891-3_24
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
