swMATH ID: 21270
Software Authors: Becker, B., Dax, C., Eisinger, J., Klaedtke, F.
Description: 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
Homepage: https://link.springer.com/chapter/10.1007/978-3-540-73368-3_36
Related Software: LASH; TaPAS; cvc3; FAST; MONA; GenPSAT; z3; SIMPLIFY; Yices; HyTech; PHAVer
Cited in: 7 Publications

Citations by Year