Maurice Laveaux: Correct and Efficient Antichain Algorithms for Refinement Checking

Event Details

Refinement checking plays an important role in system verification. This means that the correctness of the system is established by showing a refinement relation between two models; one for the implementation and one for the specification. Previously, Wang et al. presented an algorithm based on antichains to efficiently decide stable failures refinement and failures-divergences refinement. We have identified several issues pertaining to the correctness and performance of these algorithms and propose new, correct, antichain-based algorithms. Using a number of experiments we show that our algorithms outperform the original ones in terms of running time and memory usage.