Navegación

Búsqueda

Búsqueda avanzada

A tool for the automatic generation of logical models of order-sorted first-order theories

Semantics-based program analysis guarantees that the obtained knowledge about focused program features matches the real behaviour of the program. Automation of the analyses requires abstraction mechanisms to approximate the (usually undecidable) program semantics and targeted properties. In this setting, the logical notions of interpretation of a logic language and model of a theory provide an appropriate framework for abstraction in the sense that the corresponding analyses will be sound and, when relying on some decidable theory, amenable for automation. We describe a new tool, AGES, which is able to automatically generate models for order-sorted first-order theories. Such theories are very helpful in the semantic description of most programming languages. The current version of the tool systematically exploits (and relies on) the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of order-sorted signatures and also the (also ranked) predicate symbols in the language by means of appropriately adapted convex matrix interpretations. The system is available as a web application and can be used to give support to users interested in checking properties of software modules provided
that they are able to describe the property as an order-sorted first-order theory whose satisfiability guarantees the property. Examples of such properties are partial correctness, program termination, etc. The paper illustrates the use of the tool by means of simple case studies.

Automatic generation of logical models for order-sorted first-order theories in program analysis

Computations are often viewed as proofs of specific sentences in some computational logic describing the operational semantics of the programming language or computational system. Since the semantics of programs (i.e., the set of such specific sentences that are provable in the logic) is usually incomputable, and most program properties undecidable, abstraction is essential in program analysis. Abstractions can be formalized as semantic models which should be automatically generated in a push-the-button-and-wait style of program analysis and verification. We investigate the automatic generation of numerical models for order-sorted first-order logics and its use in program analysis. Our development systematically uses the recently introduced convex domains which are well-suited for representing domains for different sorts; we use them to interpret the ranked symbols of sorted signatures by means of appropriately adapted convex matrix interpretations. Such numerical interpretations permit the use of existing algorithms and tools from linear algebra (e.g., Farkas’ Lemma), real algebraic geometry, and arithmetic constraint solving in the implementation of the analyses.