Advertisement
Published in:
2011 | OriginalPaper | Chapter
An Interpolating Decision Procedure for Transitive Relations with Uninterpreted Functions
Authors : Daniel Kroening, Georg Weissenbacher
Published in: Hardware and Software: Verification and Testing
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
We present a proof-generating decision procedure for the quantifier-free fragment of first-order logic with the relations =, ≠, ≥, and > and argue that this logic, augmented with a set of theory-specific rewriting rules, is adequate for bit-level accurate verification. We describe our decision procedure from an algorithmic point of view and explain how it is possible to efficiently generate Craig interpolants for this logic.
Furthermore, we discuss the relevance of the logical fragment in software model checking and provide a preliminary evaluation of its applicability using an interpolation-based program analyser.