Naslov
Verification of an Off-Line Checker for Priority-Queues

Autori
De Nivelle, Hans ; Piskač, Ružica

Vrsta, podvrsta i kategorija rada
Radovi u zbornicima skupova, cjeloviti rad (in extenso), znanstveni

Izvornik
Proceedings of the 3d IEEE International Conference on Software Engineering and Formal Methods (SEFM) / Schmitt, Peter H ; - Los Alamitos (CA) : Institute of Electrical and Electronics Engineers (IEEE), 2005, 210-219

Skup
The 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM)

Mjesto i datum
Koblenz, Njemačka, 05.09.2005. - 09.09.2005

Vrsta sudjelovanja
Predavanje

Vrsta recenzije
Međunarodna recenzija

Ključne riječi
formal verification; result checker; priority queues; theorem proving

Sažetak
We formally verify the result checker for priority queues that is implemented in LEDA. We have developed a method, based on the notion of implementation, which links abstract specifications to concrete implementations. The method allows non-determinism in the abstract specifications that the concrete implementations have to fill in. We have formally verified that, if the checker has not reported an error up to a certain moment, then the structure it checks has behaved like a priority queue up to that moment. For the verification, we have used the first-order theorem prover Saturate.

Izvorni jezik
Engleski

Znanstvena područja
Matematika, Računarstvo

POVEZANOST RADA