Model Checking Generic Container Implementations

摘要: Model checking techniques have been successfully applied to the verification of correctness properties complex hardware systems and communication protocols. This success has fueled application these software systems. To date, those efforts targeted at concurrent whose complexity lies, primarily, in large number possible execution orderings asynchronously executing program actions. In this paper, we apply existing model parameterizable implementations container data structures. contrast most that studied literature, lies their structures algorithms. We report our experiences specifications queue, stack priority queue implemented Ada