|
Published Articles >> Table of Contents >> Abstract
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05)
pp. 210-219
Verification of an Off-Line Checker for Priority Queues
Hans De Nivelle, Max Planck Institut fur Informatik, Germany
Ruzica Piskac, Max Planck Institut fur Informatik, Germany
Full Article Text:
 
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.54
Send link to a friend
| Abstract |
|
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.
|
 Additional Information
|
Citation:
Hans De Nivelle, Ruzica Piskac,
"Verification of an Off-Line Checker for Priority Queues,"
sefm,
pp. 210-219,
Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05),
2005
|
|
