Autor:
Peña Marí, Ricardo

Foto de perfil
E-mails conocidos
ricardo@sip.ucm.es,
ricardo@sip.ucm.es
Fecha de nacimiento
Proyectos de investigación
Unidades organizativas
Puesto de trabajo
Apellidos
Peña Marí
Nombre de pila
Ricardo
Nombre
Nombres alternativos
Peña, Ricardo
Afiliaciones conocidas
Complutense University of Madrid, Spain
Universidad Complutense de Madrid, Spain
Universidad Complutense de Madrid
Páginas web conocidas
Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 201952020 - 20211
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 6 de 6
  • Miniatura
    Artículo
    Synthesizing Invariants for Arrays
    Montenegro, Manuel; Nieva, Susana; Peña Marí, Ricardo; Segura, Clara. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
    Liquid types can be seen as as a computer assisted verification system. Ordinary Hindley-Milner types are qualified by predicates expressing properties. In this way, the programmer may specify the preconditions and postconditions of functions. More importantly, the system infers the types of all the intermediate variables and checks that the verification conditions proving correctness hold. The predicates are currently expressed in a quantifier free decidable logic. Here, we extend Liquid types with quantified predicates of a decidable logic for arrays, propose a concept of an array refinement type, and provide an inference algorithm for this extension. By applying this ideas to several imperative algorithms dealing with arrays, we have been able to infer complex invariants.
  • Miniatura
    Artículo
    A Generic Intermediate Representation for Verification Condition Generation, Work in Progress
    Montenegro, Manuel; Peña Marí, Ricardo; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.
  • Miniatura
    Artículo
    Introducción a los algoritmos cuánticos
    Peña Marí, Ricardo. Actas de las XX Jornadas de Programación y Lenguajes (PROLE 2021), 2021-09-22.
    La computación cuántica ha pasado a ser un tema de actualidad desde que, en 2019, Google anunció que había ejecutado en un computador cuántico un algoritmo que llevaría miles de años a un computador convencional. Lo que el futuro deparará a esta área es todavía incierto pero, por si acaso, muchos paises están invirtiendo cuantiosas sumas en acelerar la investigación en tecnologías cuánticas. En este trabajo se presentan los fundamentos de los algoritmos cuánticos y se sugiere que una introducción a los mismos debería formar parte del curriculum académico de todos los ingenieros informáticos.
  • Miniatura
    Artículo
    Processing an Intermediate Representation Written in Lisp
    Peña Marí, Ricardo; Saavedra, Santiago; Sánchez-Hernández, Jaime. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
    In the context of designing the verification platform CAVI-ART, we arrived to the need of deciding a textual format for our intermediate representation of programs. After considering several options, we finally decided to use S-expressions for that textual representation, and Common Lisp for processing it in order to obtain the verification conditions. In this paper, we discuss the benefits of this decision. S-expressions are homoiconic, i.e. they can be both considered as data and as code. We exploit this duality, and extensively use the facilities of the Common Lisp environment to make different processing with these textual representations. In particular, using a common compilation scheme we show that program execution, and verification condition generation, can be seen as two instantiations of the same generic process.
  • Miniatura
    Artículo
    An Introduction to Liquid Haskell
    Peña Marí, Ricardo. Actas de las XVI Jornadas de Programación y Lenguajes (PROLE 2016), 2016-09-02.
    This paper is a tutorial introducing the underlying technology and the use of the tool Liquid Haskell, a type-checker for the functional language Haskell that can help programmers to verify non-trivial properties of their programs with a low effort. The first sections introduce the technology of Liquid Types by explaining its principles and summarizing how its type inference algorithm manages to prove properties. The remaining sections present a selection of Haskell examples and show the kind of properties that can be proved with the system.
  • Miniatura
    Artículo
    SMT-based Test-Case Generation with Complex Preconditions
    Peña Marí, Ricardo; Sánchez-Hernández, Jaime; Garrido, Miguel; Sagredo, Javier. Actas de las XIX Jornadas de Programación y Lenguajes (PROLE 2019), 2019-09-02.
    We present a system which can automatically generate an exhaustive set of black-box test-cases, up to a given size, for programs under test requiring complex preconditions. The key of the approach is to translate a formal precondition into a set of constraints belonging to the decidable logics of SMT solvers. By checking the satisfiability of the constraints, then the models returned by the solver automatically synthesize the cases. We also show how to use SMT solvers to automatically check for validity the test-case results, and also to complement the black-box cases with white-box ones. Finally, we use of solver to perform what we call automatic partial verification of the program. In summary, we propose a system in which exhaustive black-box and white-box testing, result checking, and partial verification, can all be done automatically. The only extra effort required from programmers is to write formal specifications.