Detail výsledku
Antichains for the Verification of Recursive Programs
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.
context free languages
regular languages
language inclusion
recursion
verification
antichains
bounded context swirthcing
Prezentujeme algoritmus pro testování inkluze jazyka bezkontextové gramatiky v jazyce konečného automatu založené na protiřetězcích, s potenciální aplikace ve verifikaci rekurzivních programů, a dále zobecnění tohoto algoritmu na omezené přepínání kontextu.
@inproceedings{BUT134220,
author="Lukáš {Holík} and Roland {Meyer} and Sebastian {Muskalla}",
title="Antichains for the Verification of Recursive Programs",
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"
}Spolehlivost a bezpečnost v IT, VUT, Vnitřní projekty VUT, FIT-S-14-2486, zahájení: 2014-01-01, ukončení: 2016-12-31, ukončen
Verifikace nekonečně stavových systémů založená na konečných automatech, GAČR, Postdoktorandské granty, GP13-37876P, zahájení: 2013-02-01, ukončení: 2015-12-31, ukončen