Recomposition: A New Technique for Efficient Compositional Verification
<|reference_start|>Recomposition: A New Technique for Efficient Compositional Verification: Compositional verification algorithms are well-studied in the context of model checking. Properly selecting components for verification is important for efficiency, yet has received comparatively less attention. In this paper, we address this gap with a novel compositional verification framework that focuses on component selection as an explicit, first-class concept. The framework decomposes a system into components, which we then recompose into new components for efficient verification. At the heart of our technique is the recomposition map that determines how recomposition is performed; the component selection problem thus reduces to finding a good recomposition map. However, the space of possible recomposition maps can be large. We therefore propose heuristics to find a small portfolio of recomposition maps, which we then run in parallel. We implemented our techniques in a model checker for the TLA+ language. In our experiments, we show that our tool achieves competitive performance with TLC-a well-known model checker for TLA+-on a benchmark suite of distributed protocols.<|reference_end|>
@article{dardik2024recomposition:,
    title={Recomposition: A New Technique for Efficient Compositional Verification},
    author={Ian Dardik, April Porter, Eunsuk Kang},
    journal={arXiv preprint arXiv:2408.03488},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.03488},
    primaryClass={cs.FL cs.LO}
}