Antichains for the verification of recursive programs

Abstract

Safety verification of while programs is often phrased in terms of inclusions L(A) ⊆ L(B) among regular languages. Antichainbased 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) ⊆ 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.