Towards verifying security policies for infinite-state systems
In International conference on verified software: Theories, tools, and experiments
Abstract
FIXME
An experience report on the optimization of the product configuration system of Renault
In Proceedings of the 26th international conference on engineering of complex computer systems (ICECCS’23)
Abstract
The problem of configuring a variability model is widespread in many different domains. A leading automobile manufacturer has developed its technology internally to model vehicle diversity. This technology relies on the approach known as knowledge compilation to explore the configurations space. However, the growing variability and complexity of the vehicles’ range hardens the space representation problem and impacts performance requirements. This paper tackles these issues by exploiting symmetries that represent isomorphic parts in the configurations space. A new method describes how these symmetries are exploited and integrated. The extensive experiments we conducted on datasets from the automobile manufacturer show our approach’s robustness and effectiveness: the achieved gain is a reduction of 52.13% in space representation and 49.81% in processing time on average
Optimization of the product configuration system of Renault
In Proceedings of the 38th ACM/SIGAPP symposium on applied computing (SAC’23)
Abstract
The problem of configuring a variability model is widespread in many different domains. Renault has developed its technology internally to model vehicle diversity. This technology relies on the approach known as knowledge compilation to explore the configurations space. However, the growing variability and complexity of the vehicles’ range hardens the space representation problem and impacts performance requirements. This paper tackles these issues by exploiting symmetries that represent isomorphic parts in the configurations space. A new method describes how these symmetries are exploited and integrated. The extensive experiments we conducted on datasets from the automobile manufacturer show our approach’s robustness and effectiveness: the achieved gain is a reduction of 52.13% in space representation on average.
Towards better heuristics for solving bounded model checking problems
In Constraints
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. We extend these study and applied the above methodology on parallel approaches, especially to refine the sharing measure which shows promising results.
Tuning SAT solvers for LTL model checking
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). By combining these two information with the classical Literal Block Distance (LBD) measure, we designed a new heuristic, well suited for solving BMC problems. In particular, our work identifies and exploits a new set of relevant (learnt) clauses. We experiment with these ideas by developing a tool dedicated for SAT-based LTL BMC solvers, called BSaLTic. Our experiments over a large database of BMC problems, show promising results. In particular, BSaLTic provides good performance on UNSAT problems. This work highlights the importance of considering the structure of the underlying problem in SAT procedures.
CosySEL: Improving SAT solving using local symmetries
In 24th international conference on verification, model checking, and abstract interpretation
Abstract
Many satisfiability problems exhibit symmetry properties. Thus, the development of symmetry exploitation techniques seems a natural way to try to improve the efficiency of solvers by preventing them from exploring isomorphic parts of the search space. These techniques can be classified into two categories: dynamic and static symmetry breaking. Static approaches have often appeared to be more effective than dynamic ones. But although these approaches can be considered as complementary, very few works have tried to combine them. In this paper, we present a new tool, CosySEL, that implements a composition of the static Effective Symmetry Breaking Predicates (esbp) technique with the dynamic Symmetric Explanation Learning (sel). esbp exploits symmetries to prune the search tree and sel uses symmetries to speed up the tree traversal. These two accelerations are complementary and their combination was made possible by the introduction of Local symmetries. We conduct our experiments on instances issued from the last ten sat competitions and the results show that our tool outperforms the existing tools on highly symmetrical problems.
Diversifying a parallel SAT solver with bayesian moment matching
In Symposium on dependable software engineering theories, tools and applications
Abstract
In this paper, we present a Bayesian Moment Matching (BMM) in-processing technique for Conflict-Driven Clause-Learning (CDCL) SAT solvers. BMM is a probabilistic algorithm which takes as input a Boolean formula in conjunctive normal form and a prior on a possible satisfying assignment, and outputs a posterior for a new assignment most likely to maximize the number of satisfied clauses. We invoke this BMM method, as an in-processing technique, with the goal of updating the polarity and branching activity scores. The key insight underpinning our method is that Bayesian reasoning is a powerful way to guide the CDCL search procedure away from fruitless parts of the search space of a satisfiable Boolean formula, and towards those regions that are likely to contain satisfying assignments.
Towards better heuristics for solving bounded model checking problems
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.
On the usefulness of clause strengthening in parallel SAT solving
In Proceedings of the 12th NASA formal methods symposium (NFM’20)
Abstract
In the context of parallel SATisfiability solving, this paper presents an implementation and evaluation of a clause strengthening algorithm. The developed component can be easily combined with (virtually) any CDCL-like SAT solver. Our implementation is integrated as a part of Painless, a generic and modular framework for building parallel SAT solvers.
Community and LBD-based clause sharing policy for parallel SAT solving
In Proceedings of the 23rd international conference on theory and applications of satisfiability testing (SAT’20)
Abstract
Modern parallel SAT solvers rely heavily on effective clause sharing policies for their performance. The core problem being addressed by these policies can be succinctly stated as “the problem of identifying high-quality learnt clauses” that when shared between the worker nodes of parallel solvers results in improved performance than otherwise. The term “high-quality clauses” is often defined in terms of metrics that solver designers have identified over years of empirical study. Some of the more well-known metrics to identify high-quality clauses for sharing include clause length, literal block distance (LBD), and clause usage in propagation. In this paper, we propose a new metric aimed at identifying high-quality learnt clauses and a concomitant clause-sharing policy based on a combination of LBD and community structure of Boolean formulas. The concept of community structure has been proposed as a possible explanation for the extraordinary performance of SAT solvers in industrial instances. Hence, it is a natural candidate as a basis for a metric to identify high-quality clauses. To be more precise, our metric identifies clauses that have low LBD and low community number as ones that are high-quality for applications such as verification and testing. The community number of a clause C measures the number of different communities of a formula that the variables in C span. We perform extensive empirical analysis of our metric and clause-sharing policy, and show that our method significantly outperforms state-of-the-art techniques on the benchmark from the parallel track of the last four SAT competitions.