Deutsch
 
Hilfe Datenschutzhinweis Impressum
  DetailsucheBrowse

Datensatz

 
 
DownloadE-Mail
  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

Externe Referenzen

einblenden:

Urheber

einblenden:
ausblenden:
 Urheber:
Piskac, Ruzica1, Autor
Ganzinger, Harald2, Ratgeber           
Podelski, Andreas2, Gutachter           
Affiliations:
1International Max Planck Research School, MPI for Informatics, Max Planck Society, Campus E1 4, 66123 Saarbrücken, DE, ou_1116551              
2Programming 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].

Details

einblenden:
ausblenden:
Sprache(n): eng - English
 Datum: 2005-02-032005
 Publikationsstatus: Erschienen
 Seiten: -
 Ort, Verlag, Ausgabe: Saarbrücken : Universität des Saarlandes
 Inhaltsverzeichnis: -
 Art der Begutachtung: -
 Identifikatoren: BibTex Citekey: Piskac2005
 Art des Abschluß: Master

Veranstaltung

einblenden:

Entscheidung

einblenden:

Projektinformation

einblenden:

Quelle

einblenden: