Verification of an Off-Line Checker for Priority Queues

Koblenz, Germany September 07-September 09

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.54

Third IEEE International Conference o ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Hans De Nivelle Articles by Ruzica Piskac

	ASCII Text	x
	Hans De Nivelle, Ruzica Piskac, "Verification of an Off-Line Checker for Priority Queues," Software Engineering and Formal Methods, International Conference on, pp. 210-219, Third IEEE International Conference on Software Engineering and Formal Methods (SEFM'05), 2005.

	BibTex	x
	@article{ 10.1109/SEFM.2005.54, author = {Hans De Nivelle and Ruzica Piskac}, title = {Verification of an Off-Line Checker for Priority Queues}, journal ={Software Engineering and Formal Methods, International Conference on}, volume = {0}, year = {2005}, isbn = {0-7695-2435-4}, pages = {210-219}, doi = {http://doi.ieeecomputersociety.org/10.1109/SEFM.2005.54}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Software Engineering and Formal Methods, International Conference on TI - Verification of an Off-Line Checker for Priority Queues SN - 0-7695-2435-4 SP210 EP219 A1 - Hans De Nivelle, A1 - Ruzica Piskac, PY - 2005 KW - null VL - 0 JA - Software Engineering and Formal Methods, International Conference on ER -

Hans De Nivelle, Max Planck Institut fur Informatik, Germany

Ruzica Piskac, Max Planck Institut fur Informatik, Germany

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.

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

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.