An Efficient Decision Procedure for the Logic of Counter Arithmetic, Constrained Lambda Expressions, Equality and Ordering with Uninterpreted Functions (CLUF)

Verifiers for infinite-state systems must trade off between the expressiveness of modeling formalism and the efficiency and automation of the tool. Efficient methods have been devised for specific classes of systems, such as super-scalar processors and systems with arbitrary size queues. However, to model systems that are combinations of these classes, no one method works well enough. In this thesis, we present CLUF..