Advertisement
Published in:
2007 | OriginalPaper | Chapter
LIRA: Handling Constraints of Linear Arithmetics over the Integers and the Reals
(Tool Paper)
Authors : Bernd Becker, Christian Dax, Jochen Eisinger, Felix Klaedtke
Published in: Computer Aided Verification
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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(ℝ, ℤ,+,<).