Arrow Research search

Author name cluster

Arnaud Gotlieb

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

13 papers
1 author row

Possible papers

13

JAIR Journal 2025 Journal Article

A Query-Based Constraint Acquisition Approach for Enhanced Precision in Program Precondition Inference

  • Grégoire Menguy
  • Sébastien Bardin
  • Arnaud Gotlieb
  • Nadjib Lazaar

Program annotations in the form of function pre/postconditions play a crucial role in various software engineering and program verification tasks. However, the frequent unavailability of these annotations necessitates manual retrofitting. This paper shows how constraint acquisition, a learning framework derived from constraint programming and version space learning, can be extended for automatically inferring program preconditions. Our approach performs this inference in a black-box manner through automatic query generation and input-output observations of program executions. We introduce PreCA, the first-ever precondition inference framework leveraging query-based constraint acquisition. Notably, we specialize PreCA to handle memory-related preconditions on binary code, which pose significant challenges in data and information management systems. In contrast to prior black-box techniques, PreCA provides well-defined guarantees. Specifically, it employs a sound and complete method to generate preconditions consistent with all the observed input-output relationships of the program. Furthermore, empirical evaluations on our benchmark demonstrate that PreCA outperforms the results of state-of-the-art approaches, delivering comparable or superior results in 5s, as opposed to the 1-hour runtime of existing approaches on identical machines. We also present two successful use cases from the standard libc and the mbedtls cryptographic library. PreCA notably infers for the former one a more precise precondition than specified in the documentation.

PDF Details DOI

JAIR Journal 2024 Journal Article

Query-driven Qualitative Constraint Acquisition

  • Mohamed-Bachir Belaid
  • Nassim Belmecheri
  • Arnaud Gotlieb
  • Nadjib Lazaar
  • Helge Spieker

Many planning, scheduling or multi-dimensional packing problems involve the design of subtle logical combinations of temporal or spatial constraints. Recently, we introduced GEQCA-I, which stands for Generic Qualitative Constraint Acquisition, as a new active constraint acquisition method for learning qualitative constraints using qualitative queries. In this paper, we revise and extend GEQCA-I to GEQCA-II with a new type of query, universal query, for qualitative constraint acquisition, with a deeper query-driven acquisition algorithm. Our extended experimental evaluation shows the efficiency and usefulness of the concept of universal query in learning randomly-generated qualitative networks, including both temporal networks based on Allen’s algebra and spatial networks based on region connection calculus. We also show the effectiveness of GEQCA-II in learning the qualitative part of real scheduling problems.

PDF Details DOI

KR Conference 2023 Conference Paper

Active Disjunctive Constraint Acquisition

  • Grégoire Menguy
  • Sébastien Bardin
  • Nadjib Lazaar
  • Arnaud Gotlieb

Constraint acquisition (CA) is a method for learning users' concepts by representing them as a conjunction of constraints. While this approach works well for many combinatorial problems over finite domains, some applications require the acquisition of disjunctive constraints, possibly coming from logical implications or negations. In this paper, we propose the first CA algorithm tailored to the automatic inference of disjunctive constraints, named DCA. A key ingredient there, is to build upon the computation of maximal satisfiable subsets. We demonstrate experimentally that DCA is faster and more effective than traditional CA with added disjunctive constraints, even for ultra-metric constraints with up to 5 variables. We also apply DCA to precondition acquisition in software verification, where it outperforms the previous CA-based approach PreCA, being 2. 5 times faster. Specifically, in our evaluation DCA infers more preconditions in just 5 minutes than PreCA does in an hour, without requiring prior knowledge about disjunction size. Our results demonstrate the potential of DCA for improving the efficiency and scalability of constraint acquisition in the disjunctive case, enabling a wide range of novel applications.

PDF Details DOI

IJCAI Conference 2022 Conference Paper

Automated Program Analysis: Revisiting Precondition Inference through Constraint Acquisition

  • Grégoire Menguy
  • Sébastien Bardin
  • Nadjib Lazaar
  • Arnaud Gotlieb

Program annotations under the form of function pre/postconditions are crucial for many software engineering and program verification applications. Unfortunately, such annotations are rarely available and must be retrofit by hand. In this paper, we explore how Constraint Acquisition (CA), a learning framework from Constraint Programming, can be leveraged to automatically infer program preconditions in a black-box manner, from input-output observations. We propose PreCA, the first ever framework based on active constraint acquisition dedicated to infer memory-related preconditions. PreCA overpasses prior techniques based on program analysis and formal methods, offering well-identified guarantees and returning more precise results in practice.

PDF Details DOI

AAAI Conference 2022 Conference Paper

GEQCA: Generic Qualitative Constraint Acquisition

  • Mohamed-Bachir Belaid
  • Nassim Belmecheri
  • Arnaud Gotlieb
  • Nadjib Lazaar
  • Helge Spieker

Many planning, scheduling or multi-dimensional packing problems involve the design of subtle logical combinations of temporal or spatial constraints. On the one hand, the precise modelling of these constraints, which are formulated in various relation algebras, entails a number of possible logical combinations and requires expertise in constraint-based modelling. On the other hand, active constraint acquisition (CA) has been used successfully to support non-experienced users in learning conjunctive constraint networks through the generation of a sequence of queries. In this paper, we propose GEQCA, which stands for Generic Qualitative Constraint Acquisition, an active CA method that learns qualitative constraints via the concept of qualitative queries. GEQCA combines qualitative queries with time-bounded path consistency (PC) and background knowledge propagation to acquire the qualitative constraints of any scheduling or packing problem. We prove soundness, completeness and termination of GEQCA by exploiting the jointly exhaustive and pairwise disjoint property of qualitative calculus and we give an experimental evaluation that shows (i) the efficiency of our approach in learning temporal constraints and, (ii) the use of GEQCA on real scheduling instances.

PDF Details

AAAI Conference 2021 Short Paper

Encoding Temporal and Spatial Vessel Context using Self-Supervised Learning Model (Student Abstract)

  • Pierre Bernabé
  • Helge Spieker
  • Bruno Legeard
  • Arnaud Gotlieb

Maritime surveillance is essential to avoid illegal activities and for environmental protection. However, the unlabeled, noisy, irregular time-series data and the large area to be covered make it challenging to detect illegal activities. Existing solutions focus only on trajectory reconstruction and probabilistic models that do ignore the context, such as the neighboring vessels. We propose a novel representation learning method that considers both temporal and spatial contexts learned in a self-supervised manner, using a selection of pretext tasks that do not require to be labeled manually. The underlying model encodes the representation of maritime vessel data compactly and effectively. This generic encoder can then be used as input for more complex tasks lacking labeled data.

PDF Details

AAAI Conference 2020 Conference Paper

Software Testing for Machine Learning

  • Dusica Marijan
  • Arnaud Gotlieb

Machine learning has become prevalent across a wide variety of applications. Unfortunately, machine learning has also shown to be susceptible to deception, leading to errors, and even fatal failures. This circumstance calls into question the widespread use of machine learning, especially in safetycritical applications, unless we are able to assure its correctness and trustworthiness properties. Software verification and testing are established technique for assuring such properties, for example by detecting errors. However, software testing challenges for machine learning are vast and profuse yet critical to address. This summary talk discusses the current state-of-the-art of software testing for machine learning. More specifically, it discusses six key challenge areas for software testing of machine learning systems, examines current approaches to these challenges and highlights their limitations. The paper provides a research agenda with elaborated directions for making progress toward advancing the state-ofthe-art on testing of machine learning.

PDF Details

AAAI Conference 2019 Conference Paper

Rotational Diversity in Multi-Cycle Assignment Problems

  • Helge Spieker
  • Arnaud Gotlieb
  • Morten Mossige

In multi-cycle assignment problems with rotational diversity, a set of tasks has to be repeatedly assigned to a set of agents. Over multiple cycles, the goal is to achieve a high diversity of assignments from tasks to agents. At the same time, the assignments’ profit has to be maximized in each cycle. Due to changing availability of tasks and agents, planning ahead is infeasible and each cycle is an independent assignment problem but influenced by previous choices. We approach the multi-cycle assignment problem as a two-part problem: Profit maximization and rotation are combined into one objective value, and then solved as a General Assignment Problem. Rotational diversity is maintained with a single execution of the costly assignment model. Our simple, yet effective method is applicable to different domains and applications. Experiments show the applicability on a multi-cycle variant of the multiple knapsack problem and a real-world case study on the test case selection and assignment problem, an example from the software engineering domain, where test cases have to be distributed over compatible test machines.

PDF Details

AAAI Conference 2018 Short Paper

Different Cycle, Different Assignment: Diversity in Assignment Problems With Multiple Cycles

  • Helge Spieker
  • Arnaud Gotlieb
  • Morten Mossige

We present approaches to handle diverse assignments in multi-cycle assignment problems. The goal is to assign a task to different agents in each cycle, such that all possible combinations are made over time. Our method combines the original profit value, that is to be optimized by the assignment problem with an additional assignment preference. By merging both, we steer the optimization towards diverse assignments without large trade-offs in the original profits.

PDF Details

AAAI Conference 2018 Conference Paper

Discovering Program Topoi Through Clustering

  • Carlo Ieva
  • Arnaud Gotlieb
  • Souhila Kaci
  • Nadjib Lazaar

Understanding source code of large open-source software projects is very challenging when there is only little documentation. New developers face the task of classifying a huge number of files and functions without any help. This paper documents a novel approach to this problem, called FEAT, that automatically extracts topoi from source code by using hierarchical agglomerative clustering. Program topoi summarize the main capabilities of a software system by presenting to developers clustered lists of functions together with an index of their relevant words. The clustering method used in FEAT exploits a new hybrid distance which combines both textual and structural elements automatically extracted from source code and comments. The experimental evaluation of FEAT shows that this approach is suitable to understand open-source software projects of size approaching 2, 000 functions and 150 files, which opens the door for its deployment in the open-source community.

PDF Details

IJCAI Conference 2017 Conference Paper

Efficient and Complete FD-solving for extended array constraints

  • Quentin Plazar
  • Mathieu Acher
  • Sébastien Bardin
  • Arnaud Gotlieb

Array constraints are essential for handling data structures in automated reasoning and software verification. Unfortunately, the use of a typical finite domain (FD) solver based on local consistency-based filtering has strong limitations when constraints on indexes are combined with constraints on array elements and size. This paper proposes an efficient and complete FD-solving technique for extended constraints over (possibly unbounded) arrays. We describe a simple but particularly powerful transformation for building an equisatisfiable formula that can be efficiently solved using standard FD reasoning over arrays, even in the unbounded case. Experiments show that the proposed solver significantly outperforms FD solvers, and successfully competes with the best SMT-solvers.

PDF Details

IJCAI Conference 2016 Conference Paper

Generating Tests for Robotized Painting Using Constraint Programming

  • Morten Mossige
  • Arnaud Gotlieb
  • Hein Meling

Designing industrial robot systems for welding, painting, and assembly, is challenging because they must perform with high precision, speed, and endurance. ABB Robotics has specialized in building highly reliable and safe robotized paint systems using an integrated process control system. However, current validation practices are mainly limited to manual test scenarios, which makes it difficult to exercise important aspects of a paint robot system, such as the need to coordinate the timing of paint activation with the robot motion control. To address these challenges, we have developed and deployed a cost-effective, automated test generation technique aimed at validating the timing behavior of the process control system. The approach is based on a constraint optimization model written in Prolog. This model has been integrated into an automated continuous integration environment, allowing the model to be solved on demand prior to test execution, which allows us to obtain the most optimal and diverse set of test scenarios for the current system configuration.

PDF Details

KER Journal 2012 Journal Article

TCAS software verification using constraint programming

  • Arnaud Gotlieb

Abstract Safety-critical software must be thoroughly verified before being exploited in commercial applications. In particular, any TCAS (Traffic Alert and Collision Avoidance System) implementation must be verified against safety properties extracted from the anti-collision theory that regulates the controlled airspace. This verification step is currently realized with manual code reviews and testing. In our work, we explore the capabilities of Constraint Programming for automated software verification and testing. We built a dedicated constraint solving procedure that combines constraint propagation with Linear Programming to solve conditional disjunctive constraint systems over bounded integers extracted from computer programs and safety properties. An experience we made on verifying a publicly available TCAS component implementation against a set of safety-critical properties showed that this approach is viable and efficient.

Details DOI