International audience

In formal methods, checking the validity of some proof obligations results in reasoning about sets, and particularly their interrelations and their cardinalities. Motivated by this interest, we investigate hybrid problems that combine constraints from both aspects. In this context, we consider two approaches: one purely qualitative and one explicitly representing membership. We propose SAT-based encodings for solving these problems. First we encode qualitative constraints on relations between sets and their cardinalities. Afterwards, we deal with richer constraints on set elements and with numerical constraints on both cardinalities and integer variables, assuming a fixed domain. In this setting, we identify a domain size bound for the version with explicit membership, beyond which increasing the domain cannot affect satisfiability. We evaluate the proposed encodings on real-world B language specifications. The proposed approaches allow the validation of proofs not yet decided by several existing approaches, and so could be used in addition to the others in order to automate the validation of even more proofs.

Boolean networks (BNs) are widely used to model biological regulatory networks. Attractors here hold significant meaning as they represent long-term behaviors such as homeostasis and the results of cell differentiation. As such, computing attractors is of critical importance to guarantee the validity of a model or to assess its stability and robustness. However, this problem is quite challenging when it comes to large real-world models. To overcome the limits of state-of-the-art BDD-based or ASP-based enumeration approaches, we introduce a SAT-based approach to compute fixed points (singleton attractors) of BN and exhibit its merits for counting the number of singleton attractors of large-scale benchmarks well established in the literature.

In this paper, we propose an enhancement to the SAT-based counterexample-guided abstraction refinement (CEGAR) approach for solving the Hamiltonian Cycle Problem (HCP). Many SAT-based methods for HCP have been proposed, including a CEGAR-based method that repeatedly solves a relaxed version of HCP strengthened by counterexamples. However, when the counterexample space - represented by the full set of subcycle partitions - is large, it becomes difficult to find a solution. To address this, we introduce cut-set constraints in the refinement step, replacing traditional subcycle blocking constraints. Our evaluation shows that these cut-set constraints achieve equal or better reduction in the counterexample space, making it easier to find valid solutions. We further assessed performance using all 1001 instances from the FHCP challenge set and confirmed that the proposed method solved 937 instances within 1800 seconds, outperforming both the existing eager and CEGAR encodings (which solved at most 666 instances). This demonstrates the effectiveness of incorporating cut-set constraints into SAT-based CEGAR approaches.

International audience

International audience

Learning pseudo-Boolean (PB) constraints in PB solvers exploiting cutting planes based inference is not as well understood as clause learning in conflict-driven clause learning solvers. In this paper, we show that PB constraints derived using cutting planes may contain irrelevant literals, i.e., literals whose assigned values (whatever they are) never change the truth value of the constraint. Such literals may lead to infer constraints that are weaker than they should be, impacting the size of the proof built by the solver, and thus also affecting its performance. This suggests that current implementations of PB solvers based on cutting planes should be reconsidered to prevent the generation of irrelevant literals. Indeed, detecting and removing irrelevant literals is too expensive in practice to be considered as an option (the associated problem is NP-hard).

We study pseudo-Boolean constraints (PBC) and their special case cardinality constraints (CARD) from the perspective of knowledge representation. To this end, the succinctness of PBC and CARD is compared to that of many standard propositional languages. Moreover, we determine which queries and transformations are feasible in polynomial time when knowledge is represented by PBC or CARD, and which are not (unconditionally or unless P = NP). In particular, the advantages and disadvantages compared to CNF are discussed.

We present a SAT-based approach for solving the modal logic S5-satisfiability problem. That problem being NP-complete, the translation into SAT is not a surprise. Our contribution is to greatly reduce the number of propositional variables and clauses required to encode the problem. We first present a syntactic property called diamond degree. We show that the size of an S5-model satisfying a formula phi can be bounded by its diamond degree. Such measure can thus be used as an upper bound for generating a SAT encoding for the S5-satisfiability of that formula. We also propose a lightweight caching system which allows us to further reduce the size of the propositional formula.We implemented a generic SAT-based approach within the modal logic S5 solver S52SAT. It allowed us to compare experimentally our new upper-bound against previously known one, i.e. the number of modalities of phi and to evaluate the effect of our caching technique. We also compared our solver againstexisting modal logic S5 solvers. The proposed approach outperforms previous ones on the benchmarks used. These promising results open interesting research directions for the practical resolution of others modal logics (e.g. K, KT, S4)

Counter-Example-Guided Abstraction Refinement (CEGAR) has been very successful in model checking large systems. Since then, it has been applied to many different problems. It especially proved to be an highly successful practical approach for solving the PSPACE complete QBF problem. In this paper, we propose a new CEGAR-like approach for tackling PSPACE complete problems that we call RECAR (Recursive Explore and Check Abstraction Refinement). We show that this generic approach is sound and complete. Then we propose a specific implementation of the RECAR approach to solve the modal logic K satisfiability problem. We implemented both a CEGAR and a RECAR approach for the modal logic K satisfiability problem within the solver MoSaiC. We compared experimentally those approaches to the state-of-the-art solvers for that problem. The RECAR approach outperforms the CEGAR one for that problem and also compares favorably against the state-of-the-art on the benchmarks considered.

We propose Nopol, an approach to automatic repair of buggy conditional statements (i.e., if-then-else statements). This approach takes a buggy program as well as a test suite as input and generates a patch with a conditional expression as output. The test suite is required to contain passing test cases to model the expected behavior of the program and at least one failing test case that reveals the bug to be repaired. The process of Nopol consists of three major phases. First, Nopol employs angelic fix localization to identify expected values of a condition during the test execution. Second, runtime trace collection is used to collect variables and their actual values, including primitive data types and objected-oriented features (e.g., nullness checks), to serve as building blocks for patch generation. Third, Nopol encodes these collected data into an instance of a Satisfiability Modulo Theory (SMT) problem; then a feasible solution to the SMT instance is translated back into a code patch. We evaluate Nopol on 22 real-world bugs (16 bugs with buggy if conditions and six bugs with missing preconditions) on two large open-source projects, namely Apache Commons Math and Apache Commons Lang. Empirical analysis on these bugs shows that our approach can effectively fix bugs with buggy if conditions and missing preconditions. We illustrate the capabilities and limitations of Nopol using case studies of real bug fixes.

Summary Variability determines the capability of software applications to be configured and customized. A common need during the development of variability‐intensive systems is the automated analysis of their underlying variability models, for example, detecting contradictory configuration options. The analysis operations that are performed on variability models are often very complex, which hinders the testing of the corresponding analysis tools and makes difficult, often infeasible, to determine the correctness of their outputs, that is, the well‐knownoracle problemin software testing. In this article, we present a generic approach for the automated detection of faults in variability analysis tools overcoming the oracle problem. Our work enables the generation of random variability models together with the exact set of valid configurations represented by these models. These test data are generated from scratch using stepwise transformations and assuring that certain constraints (a.k.a.metamorphic relations) hold at each step. To show the feasibility and generalizability of our approach, it has been used to automatically test several analysis tools in three variability domains: feature models, common upgradeability description format documents and Boolean formulas. Among other results, we detected 19 real bugs in 7 out of the 15 tools under test. Copyright © 2015 John Wiley & Sons, Ltd.

Feature-models (fms) are a widely used approach to specify the commonalities and variability in variable systems and software product lines. Various works have addressed edits to fms for fm evolution and tool support to ensure consistency of fms. An important extension to fms are feature cardinalities and related constraints, as extensively used e.g., when modeling variability of cloud computing environments. Since cardinality-based fms pose additional complexity, additional support for evolution and consistency checking with respect to feature cardinalities would be desirable, but has not been addressed yet. In this paper, we discuss common cardinality-based fm edits and resulting inconsistencies based on experiences with fms in cloud domain. We introduce tool-support for automated inconsistency detection and explanation based on an off-the-shelf solver. We demonstrate the feasibility of the approach by an empirical evaluation showing the performance of the tool.

This paper describes a logical machinery for computing decisions, where the available knowledge on the state of the world is described by a possibilistic propositional logic base (i.e., a collection of logical statements associated with qualitative c

Argument-based reasoning is a promising approach to handle inconsistent belief bases. The basic idea is to justify each plausible conclusion by acceptable arguments. The purpose of the paper is to enforce the concept of acceptability by the integration of preference orderings. Pursuing previous work on preference-based argumentation, the authors focus on the definition of preference relations for comparing conflicting arguments. They present a comparative study of several proposals. They then propose techniques for computing and comparing arguments, taking advantage of an assumption-based truth maintenance system (ATMS).