Evgenii Moiseenko. Enhancing Model Checking in Lincheck with Partial Order Reduction скачать в хорошем качестве

Evgenii Moiseenko. Enhancing Model Checking in Lincheck with Partial Order Reduction

Lincheck is a declarative framework for testing concurrent algorithms on the JVM. One of the components of this framework is the model checker, which systematically and deterministically generates different interleavings of a concurrent program for verification. The current model checking algorithm examines all possible interleavings, which is often redundant. Partial Order Reduction is a well-known technique that significantly reduces the search space by avoiding exploration of interleavings equivalent up to a permutation of commutative operations. In this talk, Evgenii will present a new model checking algorithm with partial order reduction that we have been developing recently. This algorithm builds upon state-of-the-art approaches, incorporating several novel ideas. Specifically, Evgenii will describe how we use the theory of event structures to simplify and optimize the algorithm. Lastly, Evgenii will discuss some of the technical challenges we encountered while integrating the algorithm into Lincheck, enabling the verification of real-world concurrent data structures from `java.util.concurrent`.