@inproceedings{10.1007/978-3-540-73368-3_36,
    Abstract = {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(ℝ, ℤ,+,<).},
    Address = {Berlin, Heidelberg},
    Author = {Becker, Bernd and Dax, Christian and Eisinger, Jochen and Klaedtke, Felix},
    BookTitle = {Computer Aided Verification},
    Editor = {Damm, Werner and Hermanns, Holger},
    File = {LIRA- Handling Constraints of Linear Arithmetics over the Integers and the Reals. - Becker2007\_Chapter\_LIRAHandlingConstraintsOfLinea - a - a - a - n.pdf},
    ISBN = {978-3-540-73368-3},
    Pages = {307--310},
    Publisher = {Springer Berlin Heidelberg},
    Title = {LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals},
    Year = {2007},
    date-added = {2020-02-12 11:28:22 +0100},
    date-modified = {2020-02-12 11:28:22 +0100},
    doi = {10.1007/978-3-540-73368-3_36}
}

@inproceedings{10.1007/978-3-540-73368-3_36, Abstract = {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(ℝ, ℤ,+,<).}, Address = {Berlin, Heidelberg}, Author = {Becker, Bernd and Dax, Christian and Eisinger, Jochen and Klaedtke, Felix}, BookTitle = {Computer Aided Verification}, Editor = {Damm, Werner and Hermanns, Holger}, File = {LIRA- Handling Constraints of Linear Arithmetics over the Integers and the Reals. - Becker2007_Chapter_LIRAHandlingConstraintsOfLinea - a - a - a - n.pdf}, ISBN = {978-3-540-73368-3}, Pages = {307--310}, Publisher = {Springer Berlin Heidelberg}, Title = {LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals}, Year = {2007}, date-added = {2020-02-12 11:28:22 +0100}, date-modified = {2020-02-12 11:28:22 +0100}, doi = {10.1007/978-3-540-73368-3_36} }