A temporal logic of nested calls and returns

Rajeev Alur, Kousha Etessami, P. Madhusudan

Research output: Chapter in Book/Report/Conference proceedingChapter

Abstract

Model checking of linear temporal logic (LTL) specifications with respect to pushdown systems has been shown to be a useful tool for analysis of programs with potentially recursive procedures. LTL, however, can specify only regular properties, and properties such as correctness of procedures with respect to pre and post conditions, that require matching of calls and returns, are not regular. We introduce a temporal logic of calls and returns (CARET) for specification and algorithmic verification of correctness requirements of structured programs. The formulas of CARET are interpreted over sequences of prepositional valuations 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 operator 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 modalities can be used to specify regular properties of local paths within a procedure that skip over calls to other procedures. CARET also admits the caller modality that jumps to the most recent pending call, and such caller modalities allow specification of a variety of security properties that involve inspection of the call-stack. Even though verifying context-free properties of pushdown systems is undecidable, we show that model checking CARET formulas against a pushdown model is decidable. We present a tableau construction that reduces our model checking problem to the emptiness problem for a Büchi pushdown system. The complexity of model checking CARET formulas is the same as that of checking LTL formulas, namely, polynomial in the model and singly exponential in the size of the specification.

Original languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
EditorsKurt Jensen, Andreas Podelski
PublisherSpringer
Pages467-481
Number of pages15
ISBN (Print)354021299X, 9783540212997
DOIs
StatePublished - 2004
Externally publishedYes

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2988
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'A temporal logic of nested calls and returns'. Together they form a unique fingerprint.

Cite this