Model-Checking LTL with Regular Valuations for Pushdown Systems
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F01%3A00004574" target="_blank" >RIV/00216224:14330/01:00004574 - isvavai.cz</a>
Výsledek na webu
—
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Model-Checking LTL with Regular Valuations for Pushdown Systems
Popis výsledku v původním jazyce
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the model-checking problem for LTL has been studied. In this paper we examine an extension of this, namely model-checking with regular valuations. The problem is solved via two different techniques, with an eye on efficiency - both techniques can be shown to be essentially optimal. Our methods are applicable to problems in different areas, e.g., data-flow analysis, analysis of systemswith checkpoints, etc., and provide a general, unifying and efficient framework for solving these problems.
Název v anglickém jazyce
Model-Checking LTL with Regular Valuations for Pushdown Systems
Popis výsledku anglicky
Recent works have proposed pushdown systems as a tool for analyzing programs with (recursive) procedures. In particular, the model-checking problem for LTL has been studied. In this paper we examine an extension of this, namely model-checking with regular valuations. The problem is solved via two different techniques, with an eye on efficiency - both techniques can be shown to be essentially optimal. Our methods are applicable to problems in different areas, e.g., data-flow analysis, analysis of systemswith checkpoints, etc., and provide a general, unifying and efficient framework for solving these problems.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
JC - Počítačový hardware a software
OECD FORD obor
—
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
Z - Vyzkumny zamer (s odkazem do CEZ)
Ostatní
Rok uplatnění
2001
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
Proceedings of 4th International Symposium on Theoretical Aspects of Computer Software (TACS 2001)
ISBN
3-540-42736-8
ISSN
—
e-ISSN
—
Počet stran výsledku
25
Strana od-do
316
Název nakladatele
Springer
Místo vydání
Berlin, Heidelberg, New York
Místo konání akce
Berlin, Heidelberg, New York
Datum konání akce
1. 1. 2001
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
—