Naslov
Formal Correctness of Result Checking for Priority Queues

Autori
Piskač, Ružica

Vrsta, podvrsta i kategorija rada
Ocjenski radovi, magistarski rad

Fakultet
Department of Computer Science

Mjesto
Saarbruecken

Datum
03.02

Godina
2005

Stranica
60

Mentor
Ganzinger, Harald ; Podelski, Andreas ; de Nivelle, Hans

Ključne riječi
formal correctness; formal verification; result checking; priority queue

Sažetak
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.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA