Formal Correctness of Result Checking for Priority Queues

Piskac, Ruzica

Lokale TagsFreigabegeschichteDetailsÜbersicht

Formal Correctness of Result Checking for Priority Queues

Piskac, R. (2005). Formal Correctness of Result Checking for Priority Queues. Master Thesis, Universität des Saarlandes, Saarbrücken.

Item is Freigegeben

einblenden: alle ausblenden: alle

Basisdaten

einblenden: ausblenden:

Datensatz-Permalink: https://hdl.handle.net/11858/00-001M-0000-0027-D74E-3 Versions-Permalink: https://hdl.handle.net/21.11116/0000-0003-016C-3

Genre: Hochschulschrift

ausblenden:

Urheber:
Piskac, Ruzica¹, Autor
Ganzinger, Harald¹, Ratgeber
Podelski, Andreas¹, Gutachter

Affiliations:
1Programming Logics, MPI for Informatics, Max Planck Society, ou_40045

Inhalt

einblenden:

ausblenden:

Schlagwörter: -

Zusammenfassung: We formally prove the correctness of the time super-efficient result checker
for priority queues, which is implemented in LEDA [15]. 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
[25].