Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
HOLÍK, L. MEYER, R. MUSKALLA, S.
Originální název
An Anti Chain-based Approach to Recursive Program Verification
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
Safety verification of while programs is often phrased in terms of inclusions L(A) in L(B) among regular languages. Antichain-based algorithms have been developed as an efficient method to check such inclusions. In this paper, we generalize the idea of antichain-based verification to verifying safety properties of recursive programs. To be precise, we give an antichain-based algorithm for checking inclusions of the form L(G) in L(B), where G is a context-free grammar and B is a finite automaton. The idea is to phrase the inclusion as a data flow analysis problem over a relational domain. In a second step, we generalize the approach towards bounded context switching.
Klíčová slova
context free languages regular languages language inclusion recursion verification antichains bounded context swirthcing
Autoři
HOLÍK, L.; MEYER, R.; MUSKALLA, S.
Vydáno
23. 3. 2016
Nakladatel
Springer International Publishing
Místo
Cham
ISBN
978-3-319-26849-1
Kniha
Proceedings of International Conference on Networked Systems
Edice
Lecture Notes in Computer Science (LNCS)
Strany od
322
Strany do
336
Strany počet
15
URL
https://link.springer.com/chapter/10.1007%2F978-3-319-26850-7_22
BibTex
@inproceedings{BUT134220, author="Lukáš {Holík} and Roland {Meyer} and Sebastian {Muskalla}", title="An Anti Chain-based Approach to Recursive Program Verification", booktitle="Proceedings of International Conference on Networked Systems", year="2016", series="Lecture Notes in Computer Science (LNCS)", pages="322--336", publisher="Springer International Publishing", address="Cham", doi="10.1007/978-3-319-26850-7\{_}22", isbn="978-3-319-26849-1", url="https://link.springer.com/chapter/10.1007%2F978-3-319-26850-7_22" }