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 - Reachability Analysis of Procedural Programs with Affine Integer Arithmetic

Reference:

Michael Luttenberger. Reachability analysis of procedural programs with affine integer arithmetic. In Oscar H. Ibarra and Hsu-Chun Yen, editors, Proceedings of the 11th Conference on Implementation and Application of Automata, volume 4094 of LNCS, 2006.

Abstract:

We present a tool for reachability analysis of procedural programs whose statements consist of affine equations and inequations. The algorithms use finite automata to finitely represent possibly infinite sets of both stack contents and memory valuations. We illustrate our program on some examples and compare it to Moped, a model checker for pushdown systems.

Suggested BibTeX entry:

@inproceedings{Lut06,
    author = {Michael Luttenberger},
    booktitle = {Proceedings of the 11th Conference on Implementation and Application of Automata},
    editor = {Oscar H. Ibarra and Hsu-Chun Yen},
    series = {LNCS},
    title = {Reachability Analysis of Procedural Programs with Affine Integer Arithmetic},
    volume = {4094},
    year = {2006}
}

PDF (180 kB)