Recursos de colección

RiuNet. Repositorio institucional de la Universitat de Valencia (99.709 recursos)

RiuNet es el Repositorio Institucional de la Universitat Politècnica de València, gestionado por la Biblioteca, cuyo objetivo es ofrecer acceso en Internet a la producción científica, académica y corporativa de la comunidad universitaria con la finalidad de aumentar su visibilidad y hacerla accesible y preservable.

Departamento Sistemas Informáticos y Computación (DSIC)

Mostrando recursos 1 - 6 de 6

  1. Abstract Contract Synthesis and Verification in the Symbolic K Framework

    Alpuente Frasnedo, María; Pardo Pont, Daniel; Villanueva García, Alicia
    In this article, we propose a symbolic technique that can be used for automatically inferring software contracts from programs that are written in a non-trivial fragment of C, called KernelC, that supports pointer-based structures and heap manipulation. Starting from the semantic definition of KernelC in the K semantic framework, we enrich the symbolic execution facilities recently provided by K with novel capabilities for contract synthesis that are based on abstract subsumption. Roughly speaking, we define an abstract symbolic technique that axiomatically explains the execution of any (modifier) C function by using other (observer) routines in the same program. We implemented...

  2. I.G.

    Hernández-Orallo, José
    This report summarises the key ideas for a simple concept of I.G. and its explanatory value for several areas.

  3. Static Correction of Maude Programs with Assertions

    Alpuente Frasnedo, María; Ballis, D.; Sapiña Sanchis, Julia
    In this paper, we present a novel transformation method for Maude programs featuring both automatic program diagnosis and correction. The input of our method is a reference specification A of the program behavior that is given in the form of assertions together with an overly general program R whose execution might violate the assertions. Our technique translates R into a refined program R' in which every computation is a computation in R that satisfies the assertions of A. Our correction technique is first formalized for topmost rewrite theories, and then we generalize it to larger rewrite theories that support nested structured...

  4. Magentix 2 User's Manual

    Botti Navarro, Vicente Juan; Argente Villaplana, Estefanía; Alemany Bordera, Jose; BELLVER FAUS, JOAN; BÚRDALO RAPA, LUIS ANTONIO; Carrascosa Casamayor, Carlos; CRIADO PACHECO, NATALIA; de la Fuente Anuarbe, Miguel Ángel; Del Val Noguera, Elena; Esparcia García, Sergio; Espinosa Minguet, Agustín Rafael; García Fornes, Ana María; Garcia Marques, Mª Emilia; Rarcia Pardo Gimenez de lo sGalanes, Juna Ángel; Giret Boggino, Adriana Susana; Hérnandez López, Luís; Heras Barberá, Stella María; Jordán Prunera, Jaume Magí; Jorge Cano, Javier; Julian Inglada, Vicente Javier; LÓPEZ FOGUÉS, RICARD; MEJÍAS RODRÍGUEZ, JOSÉ MANUEL; Alberola Oltra, Juan Miguel; Such Oltra, José Miguel; MULET MENGUAL, LUIS; NAVARRO LLÁCER, MARTÍN; PAJARES FERRANDO, SERGIO; Palanca Cámara, Javier; Palomares Chust, Alberto; Pérez, Pedro; Rebollo Pedruelo, Miguel; RODRIGO SOLAZ, MARIO; Ruíz, José Vicente; Soler Bayona, José Vicente; Terrasa Barrena, Andrés Martín; Valero Cubas, Soledad
    USER’S MANUAL. Version 2.1.0. January 2015

  5. ACUOS: A System for Modular ACU Generalization with Subtyping and Inheritance (extended version)

    Alpuente, María; Escobar, Santiago; Espert, Javier; Meseguer, José
    Computing generalizers is relevant in a wide spectrum of automated reasoning areas where analogical reasoning and inductive inference are needed. The ACUOS system computes a complete and minimal set of semantic generalizers (also called \anti-uni ers") of two structures in a typed language modulo a set of equational axioms. By supporting types and any combination of associativity (A), commutativity (C), and unity (U) algebraic axioms for function symbols, ACUOS allows reasoning about typed data structures, e.g. lists, trees, and (multi-)sets, and typical hierarchical/structural relations such as is a and part of. This paper discusses the modular ACU generalization tool ACUOS and illustrates its use in a classical arti ficial intelligence...

  6. Abstract Diagnosis for tccp using a Linear Temporal Logic

    COMINI, MARCO; Titolo, Laura; Villanueva García, Alicia
    Automatic techniques for program verification usually suffer the well-known state explosion problem. Most of the classical approaches are based on browsing the structure of some form of model (which rep- resents the behavior of the program) to check if a given specification is valid. This implies that a part of the model has to be built, and some- times the needed fragment is quite huge. In this work, we provide an alternative automatic decision method to check whether a given property, specified in a linear temporal logic, is valid w.r.t. a tccp program. Our proposal (based on abstract interpreta- tion techniques)...

Aviso de cookies: Usamos cookies propias y de terceros para mejorar nuestros servicios, para análisis estadístico y para mostrarle publicidad. Si continua navegando consideramos que acepta su uso en los términos establecidos en la Política de cookies.