Logical models for automated semantics-directed program analysis

Abstract

[EN] In Computer Science and Software Engineering, even at this time, when huge hardware and software resources are available, the problem of checking correctness of an specific piece of software is a very complicated one. Since the manual inspection of software is a difficult and error prone task, we propose as the main objective of this thesis the development of a tool which is able to generate logical models which can be used as a basis for semantics directed program analysis. To develop this tool, we rely on Order-Sorted First-Order Logic, which is the logic we use to define our programs and properties to be analyzed. We use this logic because it is sufficiently expressive to be used in the semantic description of most programming languages. Also, we use Convex Domain Interpretations as a flexible and computationally suitable basis for our derived models. We will also use polynomial interpretations and we will deal with conditional polynomial constraints, which are amenable for automating tests of properties written in order-sorted first-order logic. We have developed an automatic test tool, named AGES, which applies the aforementioned theoretical framework to implement the automated generation of models using convex domains and conditional polynomial constraints. The tool accepts Order-Sorted First-Order theories written in MAUDE, transforms them into a set of polynomial constraints, and then solves those constraints using an external SMT solver tool. The outcome of the constraint solver is used to assemble a logical model for the initial theory, which often can be used later to test other properties (termination, correctness, etc). The tool is written in Haskell to mutually exploit synergies between the functionalities provided by AGES and the functionalities provided by the mu-term tool.