Conference paper

HOLÍK Lukáš, MEYER Roland and MUSKALLA Sebastian. An Anti Chain-based Approach to Recursive Program Verification. In: Proceedings of International Conference on Networked Systems. Cham: Springer International Publishing, 2016, pp. 322-336. ISBN 978-3-319-26849-1. Available from: https://link.springer.com/chapter/10.1007%2F978-3-319-26850-7_22
Publication language:english
Original title:Antichains for the Verification of Recursive Programs
Title (cs):Proitiřetězce pro verifikaci rekurzivních programů
Pages:322-336
Proceedings:Proceedings of International Conference on Networked Systems
Conference:The international conference on networked systems
Series:Lecture Notes in Computer Science (LNCS)
Place:Cham, CH
Year:2016
URL:https://link.springer.com/chapter/10.1007%2F978-3-319-26850-7_22
ISBN:978-3-319-26849-1
DOI:10.1007/978-3-319-26850-7_22
Publisher:Springer International Publishing
Keywords
context free languages
regular languages
language inclusion
recursion
verification 
antichains
bounded context swirthcing
Annotation
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.
Abstract
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.
BibTeX:
@INPROCEEDINGS{
   author = {Luk{\'{a}}{\v{s}} Hol{\'{i}}k and Roland Meyer and
	Sebastian Muskalla},
   title = {Antichains for the Verification of Recursive
	Programs},
   pages = {322--336},
   booktitle = {Proceedings of International Conference on Networked Systems},
   series = {Lecture Notes in Computer Science (LNCS)},
   year = 2016,
   location = {Cham, CH},
   publisher = {Springer International Publishing},
   ISBN = {978-3-319-26849-1},
   doi = {10.1007/978-3-319-26850-7_22},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=10879}
}

Your IPv4 address: 3.81.28.94