LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals

Bernd Becker and Christian Dax and Jochen Eisinger and Felix Klaedtke

We present the tool LIRA that implements decision procedures based on automata-theoretic techniques for first-order logics with linear arithmetic over the integers and the reals. LIRA also provides an efficient automata library, which is accessible through a high-level and low-level API.

back