We present a practical algorithm for computing least solutions of systems of (fixpoint-)equations over the integers with, besides other monotone operators, addition, multiplication by positive constants, maximum, and minimum. The algorithm is based on max-strategy iteration. Its worst-case running-time (w.r.t. a uniform cost measure) is independent of the sizes of occurring numbers. We apply this algorithm to the problem of computing the abstract semantics of programs over integer intervals as well as over integer zones.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 firstname.lastname@example.org
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 email@example.com