Publication Details

Antichains for the Verification of Recursive Programs

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. Lecture Notes in Computer Science (LNCS). 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
Czech title
Proitiřetězce pro verifikaci rekurzivních programů
Type
conference paper
Language
english
Authors
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT)
Meyer Roland (UNIKL)
Muskalla Sebastian (UNIKL)
URL
Keywords

context free languages
regular languages
language inclusion
recursion
verification 
antichains
bounded context swirthcing

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.

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.

Published
2016
Pages
322-336
Proceedings
Proceedings of International Conference on Networked Systems
Series
Lecture Notes in Computer Science (LNCS)
Conference
The international conference on networked systems, Boulevard du 20 aout, Agadir, Morocco, MA
ISBN
978-3-319-26849-1
Publisher
Springer International Publishing
Place
Cham, CH
DOI
10.1007/978-3-319-26850-7_22
EID Scopus
2-s2.0-84961148811
BibTeX 
@INPROCEEDINGS{FITPUB10879,
   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 = "https://www.fit.vut.cz/research/publication/10879"
}
Back to top