Sa~zetak:
We formally prove the correctness of the time super-efficient result
checker for priority queues, which is implemented in LEDA. A priority
queue is a data structure that supports insertion, deletion and retrieval
of the minimal element, relative to some order.
A result checker for priority queues is a data structure that monitors the
input and output of the priority queue. Whenever the user requests a
minimal element, it checks that the returned element is indeed minimal. In
order to do this, the checker makes use of a system of lower bounds.
We have verified that, for every execution sequence in which the checker
accepts the outputs, the priority queue returned the correct minimal
elements. For the formal verification, we used the first-order theorem
prover Saturate.