Recomposition: A New Technique for Efficient Compositional Verification

Formal Verification

Compositional Verification

Model Checking

This project is aimed at improving compositional verification for symbolic specifications. The core idea is to decompose a symbolic specification into components, which we then recompose into components that define an efficient compositional verification problem. Recomposition is determined by a recomposition map; since there are many recomposition maps to choose from, we use heuristics to find a small portfolio of maps which we run in parallel. In our FMCAD’24 paper, we introduce the notion of recomposition and present a recomposition-based model checker for the TLA+ formal specification language.

Publications:

• Recomposition: A New Technique for Efficient Compositional Verification (to appear in FMCAD 2024)