Autor:
Abuin, Alex

Cargando...
Foto de perfil

E-mails conocidos

aabuin@ikerlan.es

Fecha de nacimiento

Proyectos de investigación

Unidades organizativas

Puesto de trabajo

Apellidos

Abuin

Nombre de pila

Alex

Nombre

Nombres alternativos

Afiliaciones conocidas

Ikerlan Research Center., Spain
Ikerlan Technology Research Center, Spain
Ik4-Ikerlan, Spain
Ik4-Ikerlan Research Center

Páginas web conocidas

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

Resultados de la búsqueda

Mostrando 1 - 2 de 2
  • Artículo
    Towards the Automatic Verification of QCSP tractability results
    Abuin, Alex; Chen, Hubie; Hermo, Montserrat; Lucio, Paqui. Actas de las XVII Jornadas de Programación y Lenguajes (PROLE 2017), 2017-07-19.
    We deal with the quantied constraint satisfaction problem (QCSP) which consists in deciding, given an structure and a rst-order sentence built from atoms, with conjunction and quantication, whether or not the sentence is true on the structure. We study a known proof system which has been used to derive QCSP tractability results. Our contribution is to formalize this proof system into an automatically veried theory, so that it can be used (in a near future) as a basis for automatically verify tractability results.
  • Artículo
    Context-based Model Checking using SMT-solvers
    Abuin, Alex; Díaz de Cerio, Unai; Hermo, Montserrat; Lucio, Paqui. Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018), 2018-09-17.
    In this paper we propose a new idea for the implementation of symbolic model checking. Our pro- posal takes advantage of two technologies. First, SMT-solvers as efficient auxiliary tools to perform a large proportion of the computational task. Second, the context-based tableau that is especially well suited for providing certificates of proved properties, as well as counterexamples of disproved properties. We mainly introduce the algorithm to be implemented, along with illustrative examples.