Note: This is an archvied version of our old webpage. Some links might be broken. The current one can be found here.
I7 Logo
Chair for Foundations of Software Reliability and Theoretical Computer Science
Informatik Logo TUM Logo
Publications - Checking System Properties via Integer Programming


S. Melzer and J. Esparza. Checking system properties via integer programming. In Proc. of ESOP'96, Lecture Notes in Computer Science. Springer-Verlag, 1996.


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.

Suggested BibTeX entry:

    author = {S. Melzer and J. Esparza},
    booktitle = {Proc. of ESOP'96},
    publisher = {{Springer-Verlag}},
    series = {{Lecture Notes in Computer Science}},
    title = {Checking System Properties via Integer Programming},
    year = {1996}

GZipped PostScript (84 kB)
PDF (331 kB)
Journal version