Partially Bounded Context-Aware Verification

Model-checking enables the formal verification of software systems. Powerful and automated, this technique suffers, however, from the state-space explosion problem because of the exponential growth in the number of states with respect to the number of interacting components. To address this problem, the Context-aware Verification (CaV) approach decomposes the verification problem using environment-based guides. This approach improves the scalability but it requires an acyclic specification of the verification guides, which are difficult to specify without losing completeness.