TY - GEN
T1 - Verification of an off-line checker for priority queues
AU - De Nivelle, Hans
AU - Piskac, Ruzica
PY - 2005
Y1 - 2005
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=84883305138&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=84883305138&partnerID=8YFLogxK
U2 - 10.1109/SEFM.2005.54
DO - 10.1109/SEFM.2005.54
M3 - Conference contribution
AN - SCOPUS:84883305138
SN - 0769524354
SN - 9780769524351
T3 - Proceedings - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005
SP - 210
EP - 219
BT - Proceedings - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005
T2 - 3rd IEEE International Conference on Software Engineering and Formal Methods, SEFM 2005
Y2 - 7 September 2005 through 9 September 2005
ER -