euforia - Complete Software Model Checking with Uninterpreted Functions.

We introduce and evaluate an algorithm for an Open image in new window -style software model checker that operates entirely at the level of equality with uninterpreted functions (EUF). Our checker, called Open image in new window , targets control properties by treating a program’s data operations/relations as uninterpreted functions/predicates. This results in an EUF abstract transition system that Open image in new window analyzes to either (1) discover an inductive strengthening EUF formula that proves the property or (2) produce an abstract counterexample that corresponds to zero, one, or many concrete counterexamples. Infeasible counterexamples are eliminated by an efficient refinement method that constrains the EUF abstraction until the property is proved or a feasible counterexample is produced. We formalize the EUF transition system, prove our algorithm correct, and demonstrate our results on a subset of benchmarks from the software verification competition (SV-COMP) 2017.