Context-based Model Checking using SMT-solvers (Trabajo en progreso)

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.

Palabras Clave:

Model checking - SAT - SMT - Solvers - Tableux

Autor(es):

• Alex Abuin {aabuin@ikerlan.es}
  Ik4-Ikerlan - Spain
  
• Unai Díaz de Cerio {udiazcerio@ikerlan.es}
  Ik4-Ikerlan - Spain
  
• Montserrat Hermo {montserrat.hermo@ehu.eus}
  University of the Basque Country (UPV/EHU) - Spain
  
• Paqui Lucio {paqui.lucio@ehu.eus}
  University of the Basque Country (UPV/EHU) - Spain
  

Handle:

Descargas:

Este artículo tiene una licencia de uso CreativeCommons - Reconocimiento (by)

Descarga el artículo haciendo click aquí.

Ver la referencia en formato Bibtex