Sign in
Author

Conference

Journal

Organization

Year

DOI
Look for results that meet for the following criteria:
since
equal to
before
between
and
Search in all fields of study
Limit my searches in the following fields of study
Agriculture Science
Arts & Humanities
Biology
Chemistry
Computer Science
Economics & Business
Engineering
Environmental Sciences
Geosciences
Material Science
Mathematics
Medicine
Physics
Social Science
Multidisciplinary
Keywords
(2)
Linear Temporal Logic
Model Checking
Related Publications
(23)
Visibly Pushdown Games
Reachability Analysis of Pushdown Automata: Application to ModelChecking
Visibly pushdown languages
Adding Nesting Structure to Words
Validating streaming XML documents
Subscribe
Academic
Publications
A Temporal Logic of Nested Calls and Returns
A Temporal Logic of Nested Calls and Returns,Rajeev Alur,Kousha Etessami,P. Madhusudan
Edit
A Temporal Logic of Nested Calls and Returns
(
Citations: 77
)
BibTex

RIS

RefWorks
Download
Rajeev Alur
,
Kousha Etessami
,
P. Madhusudan
Conference:
Tools and Algorithms for Construction and Analysis of Systems  TACAS
, pp. 467481, 2004
Cumulative
Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
(
www.springerlink.com
)
(
www.springerlink.com
)
(
www.informatik.unitrier.de
)
(
springerlink.metapress.com
)
More »
Citation Context
(62)
...There are interesting temporal logics suitable for expressing properties of singlestack pushdown systems, like the logic CARET [
4
])...
P. Madhusudan
,
et al.
The tree width of auxiliary storage
...For instance, model checking regular nestedword properties of recursive state machines, which can model control flows of imperative programs [3,
4
], and of Boolean programs [7], which are widely used as abstractions in software model checking, can be carried out in an automatatheoretic setting, similar to finitestate model checking [23]...
...a formula in a temporal logic over nested words like CaRet [
4
], NWTL [2], and μNWTL [10], is translated into a languageequivalent NWA...
...In [2,
4
], the respective authors introduce the temporal logics CaRet and...
Christian Dax
,
et al.
Alternation Elimination for Automata over Nested Words
...Such structures naturally appear in XML documents that are string representations of trees using opening and closing tags [8, 32], or in software verification of programs with stackbased control flow [2,
4
]. A nested word automaton [6] runs from left to right, similarly to a finite state automaton, but each time it encounters a “return” position, the next state depends not only on the current state but also on the state of the matching ...
...Applications in program analysis are discussed, e.g., in [2,
4
], and applications in processing treestructured data in [8, 32]...
...With the development of temporal logics for nested words [1, 2,
4
], it is natural to develop alternating automata for nested words, with the hope that they can simplify the process of translating temporal logics into automata...
Marcelo Arenas
,
et al.
Regular Languages of Nested Words: Fixed Points, Automata, and Synchro...
...The benets of this modeling have already been shown for software model checking: when all variables are boolean, viewing the program as a nitestate nestedwordautomaton generating a regular language of nested words allows model checking of nonregular temporal properties [
2
, 1, 6]...
...In a nested word, there are many notions of paths such as global, local, and staircase [
2
, 1, 13]temporal logics for nested words contain modalities such as \always" and \eventually" parameterized by the path type...
...There have been many papers on nested words and associated logics recently, but these focus on model checking (of pushdown models) and expressiveness [13,
2
, 1, 6]...
Rajeev Alur
,
et al.
Temporal Reasoning for Procedural Programs
...Researchers then considered more expressive logics that are tailored for pushdown graphs [
AEM04
] 1 and showed how to handle restricted cases of communicating pushdown systems [KIG05, BTP06, KG06, KGS06, KG07]...
...It can be easily extended to handle also CARET specifications [
AEM04
]...
...Recently, Alur et al. suggested the logic CARET, that can specify nonregular properties [
AEM04
]...
Orna Kupferman
,
et al.
An AutomataTheoretic Approach to InfiniteState Systems
References
(28)
The tempoml logic of reactive and concurrent sgstems: specification
(
Citations: 292
)
A. Pnueli
Published in 1991.
MOPS: an infrastructure for examining security properties of software
(
Citations: 253
)
Hao Chen
,
David Wagner
Conference:
ACM Conference on Computer and Communications Security  CCS
, pp. 235244, 2002
Design and synthesis of synchronization skeletons using branching time temporal logic
(
Citations: 1136
)
Edmund M. Clarke
,
E. Allen Emerson
Conference:
Logic of Programs
, pp. 5271, 1981
An overview of JML tools and applications
(
Citations: 461
)
Lilian Burdy
,
D avid Cokb
,
Michael D. Ernstd
,
Joe Kiniry
,
Rustan Leino
Journal:
Electronic Notes in Theoretical Computer Science  ENTCS
, vol. 80, 2003
Analysis of Recursive State Machines
(
Citations: 97
)
Rajeev Alur
,
Kousha Etessami
,
Mihalis Yannakakis
Conference:
Computer Aided Verification  CAV
, pp. 207220, 2001
Sort by:
Citations
(77)
The tree width of auxiliary storage
(
Citations: 2
)
P. Madhusudan
,
Gennaro Parlato
Journal:
Sigplan Notices  SIGPLAN
, pp. 283294, 2011
Alternation Elimination for Automata over Nested Words
(
Citations: 1
)
Christian Dax
,
Felix Klaedtke
Conference:
Foundations of Software Science and Computation Structure  FoSSaCS
, pp. 168183, 2011
Regular Languages of Nested Words: Fixed Points, Automata, and Synchronization
Marcelo Arenas
,
Pablo Barceló
,
Leonid Libkin
Journal:
Theory of Computing Systems / Mathematical Systems Theory  MST
, vol. 49, no. 3, pp. 639670, 2011
Temporal Reasoning for Procedural Programs
(
Citations: 2
)
Rajeev Alur
,
Swarat Chaudhuri
Conference:
Verification, Model Checking and Abstract Interpretation  VMCAI
, pp. 4560, 2010
An AutomataTheoretic Approach to InfiniteState Systems
(
Citations: 1
)
Orna Kupferman
,
Nir Piterman
,
Moshe Y. Vardi
Conference:
Birthday ...
, pp. 202259, 2010