Verification of an Off-Line Checker for Priority-Queues (CROSBI ID 511959)
Prilog sa skupa u zborniku | izvorni znanstveni rad | međunarodna recenzija
Podaci o odgovornosti
de Nivelle, Hans ; Piskač, Ružica
engleski
Verification of an Off-Line Checker for Priority-Queues
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.
formal verification; result checker; priority queues; theorem proving
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
nije evidentirano
Podaci o prilogu
210-219-x.
2005.
objavljeno
Podaci o matičnoj publikaciji
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)
Podaci o skupu
The 3rd IEEE International Conference on Software Engineering and Formal Methods (SEFM)
predavanje
05.09.2005-09.09.2005
Koblenz, Njemačka