ResumenTowards a Formal Semantics-Based Technique for Interprocedural SlicingAsavoae, 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. ResumenA Haskell Implementation of a Rule-Based Program Transformation for C ProgramsTamarit, 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. ArtículoAutomatic generation of logical models for order-sorted first-order theories in program analysisLucas, 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.