The formal analysis and verification of parallelized algorithms on list decision diagrams implemented in the Sylvan library are presented. The algorithms are parallelized by the Lace parallelization framework. Key components of Sylvan are modelled using mCRL2, a tool for analyzing concurrent systems, focusing on verifying the functional correctness of algorithms.

The analysis begins with an in-depth study of Lace, where independent task parallelization is modelled using fork-join parallelism. A key result is the development of an abstract specification for Lace, which significantly reduces the state space compared to modelling the specification of Lace while preserving correctness through branching bisimilarity. This reduction made verifying the behaviour of parallelized list decision diagram algorithms feasible. Further, Sylvan’s concurrent data structures were modelled. The specification was altered to reduce the state space while retaining behavioural equivalence with the actual specification.

Several LDD algorithms—such as cube-union, union, minus, and project—were formally verified by modelling their behaviour and applying test selection hypotheses to reduce the complexity of testing. Despite the challenges posed by the state-space explosion caused by the complexity of the specifications, the correctness of several parallelized algorithms on LDDs is demonstrated.