Proving Program Properties as First-Order Satisfiability

TL;DR

This paper extends a method for proving program properties by finding models of first-order theories, enabling broader applicability and practical use in verifying program correctness.

Contribution

It generalizes previous results to arbitrary first-order properties, allowing program verification through model finding without restrictions.

Findings

Method successfully proves properties by model finding.

Applicable to a wider class of program properties.

Practical tools can automate the verification process.

Abstract

Program semantics can often be expressed as a (many-sorted) first-order theory S, and program properties as sentences $\varphi$ which are intended to hold in the canonical model of such a theory, which is often incomputable. Recently, we have shown that properties $\varphi$ expressed as the existential closure of a boolean combination of atoms can be disproved by just finding a model of S and the negation $\neg\varphi$ of $\varphi$. Furthermore, this idea works quite well in practice due to the existence of powerful tools for the automatic generation of models for (many-sorted) first-order theories. In this paper we extend our previous result to arbitrary properties, expressed as sentences without any special restriction. Consequently, one can prove a program property $\varphi$ by just finding a model of an appropriate theory (including S and possibly something else) and an appropriate first-order formula related to $\varphi$. Beyond its possible theoretical interest, we show that our results can also be of practical use in several respects.