# Logical Characterization of Coherent Uninterpreted Programs

@article{HariGovindV2021LogicalCO, title={Logical Characterization of Coherent Uninterpreted Programs}, author={K. HariGovindV. and Sharon Shoham and A. Gurfinkel}, journal={ArXiv}, year={2021}, volume={abs/2107.12902} }

An uninterpreted program (UP) is a program whose semantics is defined over the theory of uninterpreted functions. This is a common abstraction used in equivalence checking, compiler optimization, and program verification. While simple, the model is sufficiently powerful to encode counter automata, and, hence, undecidable. Recently, a class of UP programs, called coherent, has been proposed and shown to be decidable. We provide an alternative, logical characterization, of this result… Expand

#### References

SHOWING 1-10 OF 17 REFERENCES

Decidable verification of uninterpreted programs

- Computer Science
- Proc. ACM Program. Lang.
- 2019

A subclass of programs is called coherent programs that admits decidable verification, and can be decided in Pspace, and is extended to classes of programs that are k-coherent, where k ∈ ℕ, obtained by (automatically) adding k ghost variables and assignments that make them coherent. Expand

Lifting Temporal Proofs through Abstractions

- Computer Science
- VMCAI
- 2003

This paper shows how to 'lift' a deductive proof that is generated for an abstract program back into the original program domain, relative to several types of abstraction relationships between the two programs, and develops simplifications of the lifting scheme for common types of abstractions. Expand

Checking Herbrand Equalities and Beyond

- Computer Science, Mathematics
- VMCAI
- 2005

It is shown that the problem of checking validity of positive Boolean combinations of Herbrand equalities at a given program point is decidable – even in presence of disequality guards. Expand

Witnessing Program Transformations

- Computer Science
- SAS
- 2013

This paper shows that witness generators can be implemented quite easily for a number of standard compiler optimizations; this exercise shows that stuttering simulation is a sound and complete witness format. Expand

IC3 Modulo Theories via Implicit Predicate Abstraction

- Computer Science, Mathematics
- TACAS
- 2014

A novel approach for generalizing the IC3 algorithm for invariant checking from finite-state to infinite-state transition systems, expressed over some background theories, based on a tight integration of IC3 with Implicit (predicate) Abstraction. Expand

Cover Algorithms and Their Combination

- Computer Science
- ESOP
- 2008

The study of cover is motivated by describing its applications in program analysis and verification techniques, like symbolic model checking and abstract interpretation, by providing a combination algorithm to combine the cover operations for theories that satisfy some general condition. Expand

Proof-Producing Congruence Closure

- Mathematics, Computer Science
- RTA
- 2005

An incremental congruence closure algorithm that has an additional $\mathit{Explain}$ operation is introduced, where a k-step proof can be recovered in almost optimal time (quasi-linear in k), without increasing the overall O(n log n) runtime of the fastest known congruent closure algorithms. Expand

Model Completeness, Covers and Superposition

- Computer Science
- CADE
- 2019

It is shown how covers are strictly related to model completions, a well-known topic in model theory, and the computation of covers within the Superposition Calculus is investigated, by adopting a constrained version of the calculus, equipped with appropriate settings and reduction strategies. Expand

Fast Decision Procedures Based on Congruence Closure

- Mathematics, Computer Science
- JACM
- 1980

A simple proof is given that the congruence closure algorithm provides a decision procedure for the quantifier-free theory of equality and the problem of determining the satisfiability of a conjunction of literals becomes NP-complete if the axiomatization of the theory of list structure is changed slightly. Expand

A polynomial-time algorithm for global value numbering

- Computer Science
- Sci. Comput. Program.
- 2007

A polynomial-time algorithm for global value numbering, which is the problem of discovering equivalences among program sub-expressions, is described and it is shown that there are programs for which the set of all equivalences contains terms whose value graph representation requires exponential size. Expand