Publication detail

An Anti Chain-based Approach to Recursive Program Verification

HOLÍK, L. MEYER, R. MUSKALLA, S.

Original Title

An Anti Chain-based Approach to Recursive Program Verification

Type

conference paper

Language

English

Original 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.

Keywords

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

Authors

HOLÍK, L.; MEYER, R.; MUSKALLA, S.

Released

23. 3. 2016

Publisher

Springer International Publishing

Location

Cham

ISBN

978-3-319-26849-1

Book

Proceedings of International Conference on Networked Systems

Edition

Lecture Notes in Computer Science (LNCS)

Pages from

322

Pages to

336

Pages count

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"
}

Documents

clanek.pdf