Checking system properties via integer programming

Stephan Melzer; Javier Esparza

doi:10.1007/3-540-61055-3_41

Checking system properties via integer programming

Stephan Melzer, Javier Esparza

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

16 Scopus citations

Abstract

The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.

Original language	English
Title of host publication	Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings
Editors	Hanne Riis Nielson
Publisher	Springer Verlag
Pages	250-264
Number of pages	15
ISBN (Print)	3540610553, 9783540610557
DOIs	https://doi.org/10.1007/3-540-61055-3_41
State	Published - 1996
Event	6th European Symposium on Programming Languages and Systems, ESOP 1996 - Linkoping, Sweden Duration: 22 Apr 1996 → 24 Apr 1996

Publication series

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

Conference

Conference	6th European Symposium on Programming Languages and Systems, ESOP 1996
Country/Territory	Sweden
City	Linkoping
Period	22/04/96 → 24/04/96

Access to Document

10.1007/3-540-61055-3_41

Cite this

Melzer, S., & Esparza, J. (1996). Checking system properties via integer programming. In H. R. Nielson (Ed.), Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings (pp. 250-264). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1058). Springer Verlag. https://doi.org/10.1007/3-540-61055-3_41

Melzer, Stephan ; Esparza, Javier. / Checking system properties via integer programming. Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings. editor / Hanne Riis Nielson. Springer Verlag, 1996. pp. 250-264 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{a86e531293b94692937f0d98f140f7d4,

title = "Checking system properties via integer programming",

abstract = "The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.",

author = "Stephan Melzer and Javier Esparza",

note = "Publisher Copyright: {\textcopyright} Springer-Verlag Berlin Heidelberg 1996.; 6th European Symposium on Programming Languages and Systems, ESOP 1996 ; Conference date: 22-04-1996 Through 24-04-1996",

year = "1996",

doi = "10.1007/3-540-61055-3_41",

language = "English",

isbn = "3540610553",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "250--264",

editor = "Nielson, {Hanne Riis}",

booktitle = "Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings",

}

Melzer, S & Esparza, J 1996, Checking system properties via integer programming. in HR Nielson (ed.), Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1058, Springer Verlag, pp. 250-264, 6th European Symposium on Programming Languages and Systems, ESOP 1996, Linkoping, Sweden, 22/04/96. https://doi.org/10.1007/3-540-61055-3_41

Checking system properties via integer programming. / Melzer, Stephan; Esparza, Javier.
Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings. ed. / Hanne Riis Nielson. Springer Verlag, 1996. p. 250-264 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1058).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Checking system properties via integer programming

AU - Melzer, Stephan

AU - Esparza, Javier

N1 - Publisher Copyright: © Springer-Verlag Berlin Heidelberg 1996.

PY - 1996

Y1 - 1996

N2 - The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.

AB - The marking equation is a well known verification method in the Petri net community. It has also be applied by Avrunin, Corbett et al. to automata models. It is a semidecision method, and it may fail to give an answer for some systems, in particular for those communicating by means of shared variables. In this paper, we complement the marking equation by a so called trap equation. We show that both together significantly extend the range of verifiable systems by conducting several case studies.

UR - http://www.scopus.com/inward/record.url?scp=84947901716&partnerID=8YFLogxK

U2 - 10.1007/3-540-61055-3_41

DO - 10.1007/3-540-61055-3_41

M3 - Conference contribution

AN - SCOPUS:84947901716

SN - 3540610553

SN - 9783540610557

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 250

EP - 264

BT - Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings

A2 - Nielson, Hanne Riis

PB - Springer Verlag

T2 - 6th European Symposium on Programming Languages and Systems, ESOP 1996

Y2 - 22 April 1996 through 24 April 1996

ER -

Melzer S, Esparza J. Checking system properties via integer programming. In Nielson HR, editor, Programming Languages and Systems - ESOP 1996 - 6th European Symposium on Programming, Proceedings. Springer Verlag. 1996. p. 250-264. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/3-540-61055-3_41

Checking system properties via integer programming

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this