Proceedings Article, Paper
@InProceedings
Beitrag in Tagungsband, Workshop


Show entries of:

this year (2019) | last year (2018) | two years ago (2017) | Notes URL

Action:

login to update

Options:








Author, Editor

Author(s):

Charatonik, Witold
Mukhopadhyay, Supratik
Podelski, Andreas

dblp
dblp
dblp



Editor(s):

Cortesi, Agostino

dblp

Not MPII Editor(s):

Cortesi, Agostino

BibTeX cite key*:

CharatonikMP2002

Title, Booktitle

Title*:

Compositional Termination Analysis of Symbolic Forward Analysis

Booktitle*:

Verification, Model Checking, and Abstract Interpretation. Third International Workshop, VMCAI 2002

Event, URLs

URL of the conference:


URL for downloading the paper:


Event Address*:

Venice, Italy

Language:

English

Event Date*
(no longer used):

-- January 21-22, 2002.

Organization:


Event Start Date:

21 January 2002

Event End Date:

22 January 2002

Publisher

Name*:

Springer

URL:


Address*:

Berlin, Germany

Type:


Vol, No, Year, pp.

Series:

Lecture Notes in Computer Science

Volume:

2294

Number:


Month:


Pages:

109-125

Year*:

2002

VG Wort Pages:


ISBN/ISSN:

3-540-43631-6

Sequence Number:


DOI:




Note, Abstract, ©


(LaTeX) Abstract:

Existing model checking tools for infinite state systems, such as
UPPAAL, HYTECH and KRONOS, use symbolic forward analysis, a possibly nonterminating procedure. We give termination criteria that allow us to reason compositionally about systems defined with asynchronous parallel composition; we can prove the termination of symbolic forward analysis for a composed system from the syntactic conditions satisfied by the component systems.

Our results apply to nonlinear hybrid systems; in particular to
rectangular hybrid systems, timed automata and o-minimal systems. In the case of integer-valued systems we give negative results: forward analysis is not well-suited for this class of inite-state systems.



Download
Access Level:

Public

Correlation

MPG Unit:

Max-Planck-Institut für Informatik



MPG Subunit:

Programming Logics Group

Audience:

Expert

Appearance:

MPII WWW Server, MPII FTP Server, MPG publications list, university publications list, working group publication list, Fachbeirat, VG Wort



BibTeX Entry:

@INPROCEEDINGS{CharatonikMP2002,
AUTHOR = {Charatonik, Witold and Mukhopadhyay, Supratik and Podelski, Andreas},
EDITOR = {Cortesi, Agostino},
TITLE = {Compositional Termination Analysis of Symbolic Forward Analysis},
BOOKTITLE = {Verification, Model Checking, and Abstract Interpretation. Third International Workshop, VMCAI 2002},
PUBLISHER = {Springer},
YEAR = {2002},
VOLUME = {2294},
PAGES = {109--125},
SERIES = {Lecture Notes in Computer Science},
ADDRESS = {Venice, Italy},
ISBN = {3-540-43631-6},
}


Entry last modified by Christine Kiesel, 03/12/2010
Show details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)
Hide details for Edit History (please click the blue arrow to see the details)Edit History (please click the blue arrow to see the details)

Editor(s)
Witold Charatonik
Created
09/27/2002 08:39:00 PM
Revisions
4.
3.
2.
1.
0.
Editor(s)
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Christine Kiesel
Edit Dates
04.08.2003 16:07:52
07.07.2003 15:38:56
27.06.2003 16:18:58
27.06.2003 16:17:41
27/09/2002 20:39:00
Show details for Attachment SectionAttachment Section
Hide details for Attachment SectionAttachment Section