Detail publikačního výsledku

Antichains for the Verification of Recursive Programs

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

Originální název

Antichains for the Verification of Recursive Programs

Anglický název

Antichains for the Verification of Recursive Programs

Druh

Stať ve sborníku v databázi WoS či Scopus

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.

Anglický 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

Klíčová slova v angličtině

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

Autoři

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

Rok RIV

2017

Vydáno

23.03.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="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"
}

Dokumenty

clanek