Model Generation for Quantified Formulas: A Taint-Based Approach

TL;DR

This paper introduces a generic taint-based reduction approach for generating models of quantified first-order formulas, significantly improving efficiency in software verification and bug detection tasks.

Contribution

It presents a novel reduction technique that enables model generation for quantified formulas by leveraging existing quantifier-free solvers, enhancing versatility and performance.

Findings

Significant performance improvements over existing methods

Effective model generation for quantified formulas

Reusable approach leveraging quantifier-free solvers

Abstract

We focus in this paper on generating models of quantified first-order formulas over built-in theories, which is paramount in software verification and bug finding. While standard methods are either geared toward proving the absence of solution or targeted to specific theories, we propose a generic approach based on a reduction to the quantifier-free case. Our technique allows thus to reuse all the efficient machinery developed for that context. Experiments show a substantial improvement over state-of-the-art methods.