Integrating deduction and model finding in a language independent setting

TL;DR

This paper proposes a formal framework combining satisfiability and proof calculi to enhance software analysis methods, enabling systematic construction of counterexamples and proof absence detection across various software artifacts.

Contribution

It introduces a novel integration of satisfiability sub-calculi with proof calculi within an abstract categorical setting for improved software analysis.

Findings

Formal foundation for combining model construction and proof methods

Framework supports language-independent software analysis techniques

Enhances ability to find finite counterexamples and prove absence of errors

Abstract

Software artifacts are ubiquitous in our lives being an essential part of home appliances, cars, cel phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either economical or, in the extreme, in human lives. Software analysis is an area in software engineering concerned on the application of different techniques in order to prove the (relative) absence of errors in software artifacts. In many cases these methods of analysis are applied by following certain methodological directives that ensure better results. In a previous work we presented the notion of satisfiability calculus as a model theoretical counterpart of Meseguer's proof calculus, providing a formal foundation for a variety of tools that are based on model construction. The present work shows how effective satisfiability sub-calculi, a special type of satisfiability calculi, can be combined with proof calculi, in order to provide foundations to certain methodological approaches to software analysis by relating the construction of finite counterexamples and the absence of proofs, in an abstract categorical setting.