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}
}