Infinite State Model Checking by Learning Transitive Relations
For researchers and practitioners in formal verification, this work offers a novel method to handle infinite state systems, but the improvement is incremental over existing techniques.
The paper proposes a new approach for proving safety of infinite state systems by extending the system with transitive relations until the diameter becomes finite, enabling safety verification via bounded model checking. The implementation in the tool LoAT is shown to be highly competitive with state-of-the-art methods.
We propose a new approach for proving safety of infinite state systems. It extends the analyzed system by transitive relations until its diameter D becomes finite, i.e., until constantly many steps suffice to cover all reachable states, irrespective of the initial state. Then we can prove safety by checking that no error state is reachable in D steps. To deduce transitive relations, we use recurrence analysis. While recurrence analyses can usually find conjunctive relations only, our approach also discovers disjunctive relations by combining recurrence analysis with projections. An empirical evaluation of the implementation of our approach in our tool LoAT shows that it is highly competitive with the state of the art.