Recomposition: A New Technique for Efficient Compositional Verification
| Autor: | Dardik, Ian, Porter, April, Kang, Eunsuk |
|---|---|
| Rok vydání: | 2024 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: 14 pages, 7 figures |
| Databáze: | arXiv |
| Externí odkaz: |
|