Pretražite po imenu i prezimenu autora, mentora, urednika, prevoditelja

Napredna pretraga

Pregled bibliografske jedinice broj: 220622

Verification of an Off-Line Checker for Priority-Queues


de Nivelle, Hans; Piskač, Ružica
Verification of an Off-Line Checker for Priority-Queues // Proceedings of the 3d IEEE International Conference on Software Engineering and Formal Methods (SEFM) / Schmitt, Peter H ; (ur.).
Los Alamitos, California: IEEE Computer Society Press, 2005. str. 210-219 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)


CROSBI ID: 220622 Za ispravke kontaktirajte CROSBI podršku putem web obrasca

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, California : IEEE Computer Society Press, 2005, 210-219

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

Mjesto i datum
Koblenz, Njemačka, 05-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


Projekti:
0037104

Ustanove:
Prirodoslovno-matematički fakultet, Matematički odjel, Zagreb


Citiraj ovu publikaciju:

de Nivelle, Hans; Piskač, Ružica
Verification of an Off-Line Checker for Priority-Queues // Proceedings of the 3d IEEE International Conference on Software Engineering and Formal Methods (SEFM) / Schmitt, Peter H ; (ur.).
Los Alamitos, California: IEEE Computer Society Press, 2005. str. 210-219 (predavanje, međunarodna recenzija, cjeloviti rad (in extenso), znanstveni)
De Nivelle, H. & Piskač, R. (2005) Verification of an Off-Line Checker for Priority-Queues. U: Schmitt, P. & (ur.)Proceedings of the 3d IEEE International Conference on Software Engineering and Formal Methods (SEFM).
@article{article, author = {de Nivelle, Hans and Piska\v{c}, Ru\v{z}ica}, editor = {Schmitt, P. and}, year = {2005}, pages = {210-219}, keywords = {formal verification, result checker, priority queues, theorem proving}, title = {Verification of an Off-Line Checker for Priority-Queues}, keyword = {formal verification, result checker, priority queues, theorem proving}, publisher = {IEEE Computer Society Press}, publisherplace = {Koblenz, Njema\v{c}ka} }
@article{article, author = {de Nivelle, Hans and Piska\v{c}, Ru\v{z}ica}, editor = {Schmitt, P. and}, year = {2005}, pages = {210-219}, keywords = {formal verification, result checker, priority queues, theorem proving}, title = {Verification of an Off-Line Checker for Priority-Queues}, keyword = {formal verification, result checker, priority queues, theorem proving}, publisher = {IEEE Computer Society Press}, publisherplace = {Koblenz, Njema\v{c}ka} }




Contrast
Increase Font
Decrease Font
Dyslexic Font