Extension of PyNuSMV SAT toolbox

Details

Supervisors

Pecheur, Charles

Faculty

Ecole polytechnique de Louvain

Degree label

Master [120] en sciences informatiques

Abstract

This thesis aims to extend the PyNuSMV framework with state-of-the-art techniques. PyNuSMV, developed at the Université Catholique de Louvain, is a Python framework exposing the abilities of the known NuSMV opensource model checker. Since a recent master thesis, it supports SAT-based bounded model checking in addition to BDD-based model checking. The integration of a recent award-winning SAT solver, Glucose, should speed up SAT-based model checking queries. Combined with IC3, a recent SAT-based model checking technique based on inductive reasoning, it is expected to further widen the abilities of PyNuSMV. The first part of this thesis focuses on theoretical background. Sat-based model checking is first explained with IC3 and an overview of recent SAT evolution follows, with a particular interest to Glucose. The second part explains the practical work of integration of Glucose and IC3 to PyNuSMV and shows the experimental results obtained. The completed integration of Glucose shows significant improvement when satisfying SAT-based model checking queries.