Artículo:
Context-based Model Checking using SMT-solvers

Fecha

2018-09-17

Editor

Sistedes

Publicado en

Actas de las XVIII Jornadas de Programación y Lenguajes (PROLE 2018)

Licencia Creative Commons

Resumen

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.

Descripción

Acerca de Abuin, Alex

Palabras clave

Model Checking, SAT, SMT, Solvers, Tableux
Página completa del ítem
Notificar un error en este artículo
Mostrar cita
Mostrar cita en BibTeX
Descargar cita en BibTeX