Publications

Tuning SAT solvers for LTL model checking

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.

Continue reading

CosySEL: Improving SAT solving using local symmetries

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.

Continue reading

Diversifying a parallel SAT solver with bayesian moment matching

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.

Continue reading

Energy problems in finite and timed automata with Büchi conditions

Abstract

We show how to efficiently solve energy Büchi problems in finite weighted automata and in one-clock weighted timed automata. Solving the former problem is our main contribution and is handled by a modified version of Bellman-Ford interleaved with Couvreur’s algorithm. The latter problem is handled via a reduction to the former relying on the corner-point abstraction. All our algorithms are freely available and implemented in a tool based on the open-source tools TChecker and Spot.

Continue reading

Higher-dimensional timed and hybrid automata

Abstract

We introduce a new formalism of higher-dimensional timed automata, based on Pratt and van Glabbeek’s higher-dimensional automata and Alur and Dill’s timed automata. We prove that their reachability is PSPACE-complete and can be decided using zone-based algorithms. We also extend the setting to higher-dimensional hybrid automata. The interest of our formalism is in modeling systems which exhibit both real-time behavior and concurrency. Other existing formalisms for real-time modeling identify concurrency and interleaving, which, as we shall argue, is problematic.

Continue reading

Introduction to the special issue on distributed hybrid systems

Abstract

This special issue contains seven papers within the broad subject of Distributed Hybrid Systems, that is, systems combining hybrid discrete-continuous state spaces with elements of concurrency and logical or spatial distribution. It follows up on several workshops on the same theme which were held between 2017 and 2019 and organized by the editors of this volume. The first of these workshops was held in Aalborg, Denmark, in August 2017 and associated with the MFCS conference. It featured invited talks by Alessandro Abate, Martin Fränzle, Kim G. Larsen, Martin Raussen, and Rafael Wisniewski. The second workshop was held in Palaiseau, France, in July 2018, with invited talks by Luc Jaulin, Thao Dang, Lisbeth Fajstrup, Emmanuel Ledinot, and André Platzer. The third workshop was held in Amsterdam, The Netherlands, in August 2019, associated with the CONCUR conference. It featured a special theme on distributed robotics and had invited talks by Majid Zamani, Hervé de Forges, and Xavier Urbain. The vision and purpose of the DHS workshops was to connect researchers working in real-time systems, hybrid systems, control theory, formal verification, distributed computing, and concurrency theory, in order to advance the subject of distributed hybrid systems. Such systems are abundant and often safety-critical, but ensuring their correct functioning can in general be challenging. The investigation of their dynamics by analysis tools from the aforementioned domains remains fragmentary, providing the rationale behind the workshops: it was conceived that convergence and interaction of theories, methods, and tools from these different areas was needed in order to advance the subject.

Continue reading

An efficient cascade of U-Net-like convolutional neural networks devoted to brain tumor segmentation

Abstract

Continue reading

The Dahu graph-cut for interactive segmentation on 2D/3D images

Abstract

Interactive image segmentation is an important application in computer vision for selecting objects of interest in images. Several interactive segmentation methods are based on distance transform algorithms. However, the most known distance transform, geodesic distance, is sensitive to noise in the image and to seed placement. Recently, the Dahu pseudo-distance, a continuous version of the minimum barrier distance (MBD), is proved to be more powerful than the geodesic distance in noisy and blurred images. This paper presents a method for combining the Dahu pseudo-distance with edge information in a graph-cut optimization framework and leveraging each’s complementary strengths. Our method works efficiently on both 2D/3D images and videos. Results show that our method achieves better performance than other distance-based and graph-cut methods, thereby reducing the user’s efforts.

Continue reading

Blockchain-based solution for detecting and preventing fake check scams

Abstract

Fake check scam is one of the most common attacks used to commit fraud against consumers. This fraud is particularly costly for victims because they generally lose thousands of dollars as well as being exposed to judicial proceedings. Currently, there is no existing solution to authenticate checks and detect fake ones instantly. Instead, banks must wait for a period of more than 48 h to detect the scam. In this context, we propose a blockchain-based scheme to authenticate checks and detect fake check scams. Moreover, our approach allows the revocation of used checks. More precisely, our approach helps the banks to share information about provided checks and used ones, without exposing the banks’ customers’ personal data. We demonstrate a proof of concept of our proposed approach using Namecoin and Hyperledger blockchain technologies.

Continue reading

Pictograms to aid laypeople in identifying the addictiveness of gambling products (PictoGRRed study)

Abstract

The structural addictive characteristics of gambling products are important targets for prevention, but can be unintuitive to laypeople. In the PictoGRRed (Pictograms for Gambling Risk Reduction) study, we aimed to develop pictograms that illustrate the main addictive characteristics of gambling products and to assess their impact on identifying the addictiveness of gambling products by laypeople. We conducted a three-step study: (1) use of a Delphi consensus method among 56 experts from 13 countries to reach a consensus on the 10 structural addictive characteristics of gambling products to be illustrated by pictograms and their associated definitions, (2) development of 10 pictograms and their definitions, and (3) study in the general population to assess the impact of exposure to the pictograms and their definitions (n = 900). French-speaking experts from the panel assessed the addictiveness of gambling products (n = 25), in which the mean of expert’s ratings was considered as the true value. Participants were randomly provided with the pictograms and their definitions, or with a standard slogan, or with neither (control group). We considered the control group as representing the baseline ability of laypeople to assess the addictiveness of gambling products. Each group and the French-speaking experts rated the addictiveness of 14 gambling products. The judgment criterion was the intraclass coefficients (ICCs) between the mean ratings of each group and the experts, reflecting the level of agreement between each group and the experts. Exposure to the pictograms and their definition doubled the ability of laypeople to assess the addictiveness of gambling products compared with that of the group that read a slogan or the control group (ICC = 0.28 vs. 0.14 (Slogan) and 0.14 (Control)). Laypeople have limited awareness of the addictive characteristics of gambling products. The pictograms developed herein represent an innovative tool for universally empowering prevention and for selective prevention.

Continue reading