de.mpg.escidoc.pubman.appbase.FacesBean
English
 
Help Guide Disclaimer Contact us Login
  Advanced SearchBrowse

Item

ITEM ACTIONSEXPORT

Released

Thesis

Formal correctness of Result Checking for Priority Queues

MPS-Authors

Piskac,  Ruzica
International Max Planck Research School, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons44474

Ganzinger,  Harald
Programming Logics, MPI for Informatics, Max Planck Society;

http://pubman.mpdl.mpg.de/cone/persons/resource/persons45201

Podelski,  Andreas
Programming Logics, MPI for Informatics, Max Planck Society;

Locator
There are no locators available
Fulltext (public)
There are no public fulltexts available
Supplementary Material (public)
There is no public supplementary material available
Citation

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


Cite as: http://hdl.handle.net/11858/00-001M-0000-0027-D74E-3
Abstract
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].