View Full Document

Join Algorithms for the Theory of Uninterpreted Functions



View the full content.
View Full Document
View Full Document

13 views

Unformatted text preview:

Join Algorithms for the Theory of Uninterpreted Functions Sumit Gulwani1 Ashish Tiwari2 and George C Necula1 1 University of California Berkeley CA 94720 gulwani necula cs berkeley edu 2 SRI International Menlo Park CA 94025 tiwari csl sri com Abstract The join of two sets of facts E1 and E2 is defined as the set of all facts that are implied independently by both E1 and E2 Congruence closure is a widely used representation for sets of equational facts in the theory of uninterpreted function symbols UFS We present an optimal join algorithm for special classes of the theory of UFS using the abstract congruence closure framework Several known join algorithms which work on a strict subclass can be cast as specific instantiations of our generic procedure We demonstrate the limitations of any approach for computing joins that is based on the use of congruence closure We also mention some interesting open problems in this area 1 Introduction Computational logic is used extensively in formal modeling and analysis of systems particularly in areas such as verification of hardware and software systems and program analysis A wide variety of logical theories are used for this purpose However even for the simplest of theories reasoning on formulas in the presence of the conjunction and disjunction connectives is computationally hard Unsurprisingly therefore almost all practical uses of logical computation have come in the form of decision procedures that work on facts stored as conjunctions of atomic formulas What happens when the application requires the computation of the logical disjunction of two such facts Join algorithms provide an approximate solution by constructing a conjunction of atomic formulas that is implied by the original disjunction Join algorithms were first studied in the context of program analysis Abstract interpretation 5 is a well known static program analysis technique that can be used to automatically generate program invariants and to verify program



Access the best Study Guides, Lecture Notes and Practice Exams

Loading Unlocking...
Login

Join to view Join Algorithms for the Theory of Uninterpreted Functions and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Join Algorithms for the Theory of Uninterpreted Functions and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?