@InProceedings{   HolikMeyer:NETYS:2015,
  Author        = "Hol{\'\i}k, Luk{\'a}{\v{s}} and Meyer, Roland",
  Editor        = "Bouajjani, Ahmed and Fauconnier, Hugues",
  Abstract      = "Safety verification of while programs is often phrased in terms of inclusions {\$}{\$}L(A){\backslash}subseteq L(B){\$}{\$}L(A)⊆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){\backslash}subseteq L(B){\$}{\$}L(G)⊆L(B), where {\$}{\$}G{\$}{\$}Gis a context-free grammar and {\$}{\$}B{\$}{\$}Bis 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.",
  Address       = "Cham",
  BookTitle     = "Proc. of NETYS'15",
  date-added    = "2018-10-25 09:02:10 +0200",
  date-modified = "2020-05-14 18:05:45 +0200",
  ISBN          = "978-3-319-26850-7",
  Pages         = "322--336",
  Publisher     = "Springer International Publishing",
  Title         = "Antichains for the Verification of Recursive Programs",
  Year          = "2015",
  File          = "HolikMeyerNetys2015 (0) - a - a - d.pdf"
}

@InProceedings{ HolikMeyer:NETYS:2015, Author = "Hol{\'\i}k, Luk{\'a}{\v{s}} and Meyer, Roland", Editor = "Bouajjani, Ahmed and Fauconnier, Hugues", Abstract = "Safety verification of while programs is often phrased in terms of inclusions {\$}{\$}L(A){\backslash}subseteq L(B){\$}{\$}L(A)⊆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){\backslash}subseteq L(B){\$}{\$}L(G)⊆L(B), where {\$}{\$}G{\$}{\$}Gis a context-free grammar and {\$}{\$}B{\$}{\$}Bis 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.", Address = "Cham", BookTitle = "Proc. of NETYS'15", date-added = "2018-10-25 09:02:10 +0200", date-modified = "2020-05-14 18:05:45 +0200", ISBN = "978-3-319-26850-7", Pages = "322--336", Publisher = "Springer International Publishing", Title = "Antichains for the Verification of Recursive Programs", Year = "2015", File = "HolikMeyerNetys2015 (0) - a - a - d.pdf" }