Anissa Kheireddine

Towards better heuristics for solving bounded model checking problems

Abstract This paper presents a new way to improve the performance of the SAT-based bounded model checking problem on sequential and parallel procedures by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approaches with two new heuristics for sequential procedures: Structure-based and Linear Programming heuristics.

Continue reading

Tuning SAT solvers for LTL model checking

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2022-12-09

In Proceedings of the 29th asia-pacific software engineering conference (APSEC’22)

Abstract Bounded model checking (BMC) aims at checking whether a model satisfies a property. Most of the existing SAT-based BMC approaches rely on generic strategies, which are supposed to work for any SAT problem. The key idea defended in this paper is to tune SAT solvers algorithm using: (1) a static classification based on the variables used to encode the BMC into a Boolean formula; (2) and use the hierarchy of Manna&Pnueli that classifies any property expressed through Linear-time Temporal Logic (LTL).

Continue reading

Towards better heuristics for solving bounded model checking problems

By Anissa Kheireddine, Étienne Renault, Souheib Baarir

2021-08-31

In Proceedings of the 27th international conference on principles and practice of constraint programmings (CP’21)

Abstract This paper presents a new way to improve the performance of the SAT-based bounded model checking problem by exploiting relevant information identified through the characteristics of the original problem. This led us to design a new way of building interesting heuristics based on the structure of the underlying problem. The proposed methodology is generic and can be applied for any SAT problem. This paper compares the state-of-the-art approach with two new heuristics: Structure-based and Linear Programming heuristics and show promising results.

Continue reading