A temporal logic of nested calls and returns

Abstract. Model checking of linear temporal logic (LTL) specications with respect to pushdown systems has been shown to be a useful tool for analysis of programs with potentially recursive procedures. LTL, how-ever, can specify only regular properties, and properties such as correct-ness of procedures with respect to pre and post conditions, that require matching of calls and returns, are not regular. We introduce a tempo-ral logic of calls and returns (CaRet) for specication and algorithmic veri cation of correctness requirements of structured programs. The for-mulas of CaRet are interpreted over sequences of propositional valu-ations tagged with special symbols call and ret. Besides the standard global temporal modalities, CaRet admits the abstract-next operator that allows a path to jump from a call to the matching return. This op-erator can be used to specify a variety of non-regular properties such as partial and total correctness of program blocks with respect to pre and post conditions. The abstract versions of the other temporal modalitie