Detail publikace

Proving Termination of Tree Manipulating Programs

HABERMEHL Peter, IOSIF Radu, ROGALEWICZ Adam a VOJNAR Tomáš. Proving Termination of Tree Manipulating Programs. In: Automated Technology for Verification and Analysis. Lecture Notes in Computer Science, roč. 4762. Berlin: Springer Verlag, 2007, s. 145-161. ISBN 978-3-540-75595-1.
Název česky
Dokazování konečnosti běhu programů manipulujících stromové struktury
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Habermehl Peter (UPAR7)
Iosif Radu (VERIMAG)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Abstrakt

Článek navrhuje metodu automatického dokazování konečnosti běhu programů manipulujících stromové struktury, založenou na využití teorie automatů. Konkrétně je pro úvodní fázi metody, ve které se generují invarianty programů, použit abstraktní stromový regulární model checking založený na stromových automatech. Pro následnou fázi verifikace konečnosti programů je využit překlad do čítačových automatů.

Rok
2007
Strany
145-161
Sborník
Automated Technology for Verification and Analysis
Řada
Lecture Notes in Computer Science
Svazek
4762
Konference
5th International Symposium on Automated Technology for Verification and Analysis -- ATVA 2007, Tokyo, JP
ISBN
978-3-540-75595-1
Vydavatel
Springer Verlag
Místo
Berlin, DE
BibTeX
@INPROCEEDINGS{FITPUB8510,
   author = "Peter Habermehl and Radu Iosif and Adam Rogalewicz and Tom\'{a}\v{s} Vojnar",
   title = "Proving Termination of Tree Manipulating Programs",
   pages = "145--161",
   booktitle = "Automated Technology for Verification and Analysis",
   series = "Lecture Notes in Computer Science",
   volume = 4762,
   year = 2007,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-540-75595-1",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8510"
}
Nahoru