Analysis and Transformation

URI permanente para esta colección:

https://hdl.handle.net/11705/1942
Artículos en la categoría Analysis and Transformation publicados en las Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015).

Examinar

Examinando Analysis and Transformation por Fecha de publicación

Filtrar resultados por año o por mes:
Mostrando 1 - 3 de 3
  • Miniatura
    Artículo
    Automatic generation of logical models for order-sorted first-order theories in program analysis
    Lucas, Salvador. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    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.
  • Miniatura
    Resumen
    A Haskell Implementation of a Rule-Based Program Transformation for C Programs
    Tamarit, Salvador; Vigueras, Guillermo; Carro, Manuel; Mariño, Julio. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    Obtaining good performance when programming heterogeneous computing platforms poses significant challenges for the programmer. We present a program transformation environment, implemented in Haskell, where architecture-agnostic scientific C code is transformed into a functionally equivalent one better suited for a given platform. The transformation rules are formalized in a domain-specific language (STML) that takes care of the syntactic and semantic conditions required to apply a given transformation. STML rules are compiled into Haskell function definitions that operate at AST level. Program properties, to be matched with rule conditions, can be automatically inferred or, alternatively, stated as annotations in the source code. Early experimental results are described.
  • Miniatura
    Resumen
    Towards a Formal Semantics-Based Technique for Interprocedural Slicing
    Asavoae, Irina Mariuca; Asavoae, Mihail; Riesco, Adrián. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    Interprocedural slicing is a technique applied on programs with procedures which relies on how the information is passed at procedure call/return sites. Such a technique computes program slices (i.e. program fragments restricted w.r.t. a given criterion). The existing approaches to interprocedural slicing exploit the particularities of the underlying language semantics in order to compute program slices. In this paper we propose a generic technique for interprocedural slicing. More specifically, our approach works with inferred particularities of a language semantics, given as a rewriting-logic specification, and computes program slices using a term slicing-based algorithm.