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