|
Abstract : |
Abstract. UCLID is a tool for specifying and verifying systems expressed in a quantier-free rst-order logic, called CLU logic, that includes uninterpreted functions, equality, ordering, constrained lambda expressions, and counter arithmetic. In previous work, we presented different variants of a decision procedure for this logic that are all based on on an ecient translation of a CLU formula to a Boolean formula, which is checked using a Boolean satisability solver. In this paper, we present another variant based on the PBS tool that integrates a pseudo-Boolean constraint solver with a SAT solver. We then present an empirical evaluation of all decision procedure variants on a set of benchmark formulas generated from various UCLID models. 1, |
