LIRA

LIRA: Handling constraints of linear arithmetics over the integers and the reals. The mechanization of many verification tasks relies on efficient implementations of decision procedures for fragments of first-order logic. Interactive theorem provers like pvs also make use of such decision procedures to increase the level of automation. Our tool lira implements decision procedures based on automata-theoretic techniques for first-order logics with linear arithmetic, namely, for FO(ℕ, +), FO(ℤ,+,<), and FO(ℝ, ℤ,+,<). This work was supported by the German Research Foundation (DFG) and the Swiss National Science Foundation (SNF). lira is available at http://lira.gforge.avacs.org/ under the GNU public licence