Autor:
Villanueva, Alicia

Foto de perfil
E-mails conocidos
villanue@dsic.upv.es
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Villanueva
Nombre de pila
Alicia
Nombre
Nombres alternativos
Afiliaciones conocidas
Universitat Politècnica de València, Spain
DSIC, Universitat Politècnica de València
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 20192
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • Miniatura
    Artículo
    Inferring Specifications in the K framework
    Alpuente, María; Pardo, Daniel; Villanueva, Alicia. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    Despite its many unquestionable benefits, formal specifications are not widely used in industrial software development. In order to reduce the time and effort required to write formal specifications, in this paper we propose a technique for automatically discovering specifications from real code. The proposed methodology relies on the symbolic execution capabilities recently provided by the K framework that we exploit to automatically infer formal specifications from programs that are written in a non–trivial fragment of C, called KERNELC. Roughly speaking, our symbolic analysis of KERNELC programs explains the execution of a (modifier) function by using other (observer) routines in the program. We implemented our technique in the automated tool KINDSPEC 2.0, which generates axioms that describe the precise input/output behavior of C routines that handle pointerbased structures (i.e., result values and state change). We describe the implementation of our system and discuss the differences w.r.t. our previous work on inferring specifications from C code.
  • Miniatura
    Artículo
    Towards a bottom-up fixpoint semantics that models the behavior of PROMELA programs
    Comini, Marco; Comisso, Francesco Saverio; Villanueva, Alicia. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.
    PROMELA (Process Meta Language) is a high-level specification language designed for modeling interactions in distributed systems. PROMELA is used as the input language for the model checker SPIN (Simple Promela INterpreter). The main characteristics of PROMELA are non-determinism, process communication through synchronous as well as asynchronous channels, and the possibility to dynamically create instances of processes. In this paper, we introduce a bottom-up, fixpoint semantics that models the behavior of PROMELA programs. This work is the first step for a more ambitious goal where analysis and verification techniques based on abstract interpretation would be defined on top of such semantics.