Valentin Montmirail (CRIL, UArtois)

We present our work toward a rigorous experimental comparison of the state of the art for the practical resolution of the satisfiability of formulae in modal logic K. Our aim is to provide a way to practically verify the answers provided by those solvers.

For this purpose, we propose a certificate format and a checker to validate Kripke models for modal logic K. We present experimental results using state-of-the-art solvers, modified to incorporate this verification step. We were able to validate 67,23 percent of the Kripke models returned by the modified solvers, which provides a set of benchmark with independently checked solution which can be used to validate new solvers.