Proving program properties as first-order satisfiability

DOI10.1007/978-3-030-13838-7_1MaRDI QIDQ6085973zbMATH OpenOpenAlexFDO

Authors Salvador Lucas

Publication date 9 November 2023

Published in Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1808.04111

zbMATH Keywords

first-order logiclogical modelsprogram analysis

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

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 $egvarphi$ 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.

Recommendations

• Proving semantic properties as first-order satisfiability
• Analysis of rewriting-based systems as first-order theories
• Automatic synthesis of logical models for order-sorted first-order theories
• Proving Properties of Constraint Logic Programs by Eliminating Existential Variables
• Software model checking by program specialization

Cited in

(3)

• Proving semantic properties as first-order satisfiability
• Automatic generation of logical models with AGES
• Proof methods of declarative properties of definite programs

This page was built for publication: Proving program properties as first-order satisfiability

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6085973)