Integrating deduction and model finding in a language independent setting

LOPEZ POMBO, CARLOS GUSTAVO; MARTINEZ SUÑÉ, AGUSTÍN ELOY

Mathematical Foundations of Software Engineering - Essays in Honour of Tom Maibaum on the Occasion of his 70th Birthday and Retirement

College Publications

Lugar: Londres; Año: 2022; p. 22 - 59

Software artifacts are ubiquitous in our lives being an essential part of home appli- ances, cars, cel phones, and even in more critical activities like aeronautics and health sciences. In this context software failures may produce enormous losses, either eco- nomical 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 cal- culus, 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 satis- fiability 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.