Autor:
Sánchez-Hernández, Jaime

Foto de perfil

E-mails conocidos

jaime@sip.ucm.es

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Sánchez-Hernández

Nombre de pila

Jaime

Nombre

Nombres alternativos

Afiliaciones conocidas

Complutense University of Madrid, Spain
Facultad de Informática Universidad Complutense de Madrid, Spain
Universidad Complutense de Madrid, Spain

Páginas web conocidas

Página completa del ítem
Notificar un error en este autor

Filtros

2015 - 20194
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 4 de 4
  • 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
    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
    HR-SQL: An SQL Database System with Extended Recursion and Hypothetical Reasoning
    Nieva, Susana; Saenz-Perez, Fernando; Sánchez-Hernández, Jaime. Actas de las XV Jornadas de Programación y Lenguajes (PROLE 2015), 2015-09-15.
    In a former work we described the system and language R-SQL that overcomes some limitations of recursion of the relational database language SQL. Such limitations are non-linearity, mutual recursion, and some combinations of negation with recursion. In addition, R-SQL improved termination properties of recursive definitions. Next, this language was extended to include a restricted form of hypothetical relations and queries using assumptions, obtaining the language HR-SQL, and a preliminary implementation was developed for it. Here, we develop a new system HR-SQL from scratch and enhance the former system in several areas. First, hypothetical reasoning is fully integrated with recursive definitions. Second, the Python script generated by the system for computing the extension (materialization) of a database is now targeted to several state-of-the-art relational database systems. Third, the system has been interfaced to the integrated development environment ACIDE, allowing both a more friendly user interaction and a graphical view of the dependency graph that shows dependencies between relations. Fourth, being developed in Prolog, we have targeted it to both SICStus Prolog and SWI-Prolog, also providing standalone executables. Finally, the system has been extended with a bundle of commands, highly improving its capabilities with respect to the former 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.