Autor:
Sagredo, Javier

Foto de perfil

E-mails conocidos

jasataco@gmail.com

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Sagredo

Nombre de pila

Javier

Nombre

Nombres alternativos

Afiliaciones conocidas

Universidad Complutense de Madrid, Spain

Páginas web conocidas

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

Filtros

20191
Restablecer filtros

Ajustes

Resultados de la búsqueda

Mostrando 1 - 1 de 1
  • 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.