EDBT 2026 Demo / reviewers in the wild / expert
Maxime Cordy
dblp:73/10839
· DBLP profile ↗
85ranked-venue papers
12as first author
56since 2021 · last 2026
0000-0001-8312-1358ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 68 · 11 first-author · 42 since 2021Artificial intelligence and machine learning · 20 · 3 first-author · 15 since 2021Databases, data management, data science and information retrieval · 4 · 2 since 2021Graphics, computer vision, multimedia, augmented reality and games · 4 · 4 since 2021Applied, interdisciplinary, general and emerging computing · 4 · 3 first-authorSecurity and privacy · 1 · 1 since 2021Theory of computation · 1 · 1 first-author · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2026 | On the Evaluation of Capability Estimation Methods for Large Language ModelsabstractThe emergence of large language models (LLMs) marks a transformative era in artificial intelligence~(AI). However, systematically evaluating the capability of LLMs is challenging due to the necessity of a large number of labeled test data. To tackle this problem, in the conventional AI field, AutoEval has been proposed to estimate the capability of AI models without data labeling effort. Unfortunately, even though multiple AutoEval methods have been proposed, most are constructed for classification tasks and evaluated only on image datasets. As a result, their effectiveness for LLMs is unclear, as LLMs often target generation tasks. In this work, we introduce the first AutoEval benchmark specifically designed to estimate the capability of LLMs using unlabeled test data, AEBench. Besides existing AutoEval methods, AEBench also supports our designed method, which utilizes the correlation between data uncertainty and model ability for the capability estimation. In total, AEBench covers 12 AutoEval methods and 120 method combinations. Based on AEBench, we conducted a comprehensive study to explore the usefulness of AutoEval on LLMs. Experimental results on 10 datasets demonstrated that our designed uncertainty features-based methods perform the best in achieving the lowest estimation errors. Maxime Cordy, Yongqiang Lyu 0003 |
AAAI | 4 |
| 2026 | DivKC: A Divide-and-Conquer Approach to Knowledge Compilation
Olivier Zeyen, Karim Tit, Maxime Cordy, Gilles Perrouin |
FASE | 3 |
| 2026 | GenCode: A generic data augmentation framework for boosting deep learning-based code understanding
Zeming Dong, Xiaofei Xie, Maxime Cordy, Mike Papadakis, Yves Le Traon, Jianjun Zhao 0001 |
Empir. Softw. Eng. | 4 |
| 2026 | AutoAdapt: On the Application of AutoML for Parameter-Efficient Fine-Tuning of Pre-Trained Code ModelsabstractLarge Language Models (LLMs) have demonstrated their ability to solve tasks across various domains, including software engineering. However, their extensive number of parameters makes full fine-tuning computationally prohibitive. While Parameter-Efficient Fine-Tuning (PEFT) methods, such as adapter fine-tuning, have been proposed to address this issue, yet they typically employ default configurations that use the same adapter settings across all layers. Concurrently, Automated Machine Learning (AutoML) has demonstrated success in hyperparameter optimization, while Neural Architecture Search (NAS) has proven effective in optimizing neural network architectures. Building on these successes, we introduce AutoAdapt, a novel approach that leverages NAS to automatically discover task-specific, layer-wide adapter configurations, allowing each layer to adopt distinct adapter parameters. AutoAdapt defines a search space tailored for adapter-based fine-tuning and employs an evolutionary algorithm to explore a diverse range of configurations, thereby evaluating the benefits of customizing each layer individually. We evaluate AutoAdapt on well-established software engineering tasks, including vulnerability detection, code clone detection, and code search. Our empirical results demonstrate that AutoAdapt outperforms manually engineered adapter configurations, achieving up to a 5% improvement in F1-score for clone detection and defect detection, and up to a 25% improvement in MRR for code search. Additionally, it surpasses other PEFT techniques, such as Prefix Tuning and LoRA. Furthermore, AutoAdapt is capable of identifying configurations that outperform even full fine-tuning, while training less than 2.5% of the model parameters. A comprehensive analysis reveals that factors such as selective layer adaptation, module selection (e.g., attention versus feed-forward layers), normalization, and dropout significantly influence performance across different tasks. Additionally, our findings suggest the possibility of transferring adapter configurations to similar datasets and tasks, thus simplifying the search for optimal PEFT settings. Our code and data are available for access at: https://github.com/serval-uni-lu/AutoAdapt . Amal Akli, Maxime Cordy, Mike Papadakis, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 2 |
| 2026 | Variable Renaming-Based Adversarial Test Generation for Code Model: Benchmark and EnhancementabstractRobustness testing is essential for evaluating deep learning models, particularly under unforeseen circumstances. Adversarial test generation, a fundamental approach in robustness testing, is prevalent in computer vision and natural language processing, and it has gained considerable attention in code tasks recently. The Variable Renaming-Based Adversarial Test Generation (VRTG), which deceives models by altering variable names, is a key focus. VRTG involves substitution construction and variable name searching, but its systematic design remains a challenge due to the empirical nature of these components. This article introduces the first benchmark to examine the impact of various substitutions and search algorithms on VRTG effectiveness, exploring improvements for existing VRTGs. Our benchmark includes three substitution construction types, six substitution position rank ways and seven search algorithms. Analysis of four code understanding tasks and three pre-trained code models using our benchmark reveals that combining RNNS and Genetic Algorithm with code-based substitution is more effective for VRTG construction. Notably, this method outperforms the advanced black-box variable renaming test generation technique, ALERT, by up to 22.57%. Yuejun Guo 0001, Maxime Cordy, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2026 | CodeS+: Towards Assessing the Generalization Ability of Code Models Under Distribution Shift
Ziyue Shi, Junjie Wang 0007, Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Sen Chen 0001, Mike Papadakis, Yves Le Traon, Yongqiang Lyu 0001 |
IEEE Trans. Software Eng. | 6 |
| 2025 | Boosting source code learning with text-oriented data augmentation: an empirical study
Zeming Dong, Yuejun Guo 0001, Zhenya Zhang 0001, Maxime Cordy, Mike Papadakis, Yves Le Traon, Jianjun Zhao 0001 |
Empir. Softw. Eng. | 5 |
| 2025 | Evaluation and Improvement of Test Selection for Large Language ModelsabstractABSTRACT Large language models (LLMs) have recently achieved significant success across various application domains, garnering substantial attention from different communities. Unfortunately, many faults still exist that LLMs cannot properly predict. Such faults will harm the usability of LLMs in general and could introduce safety issues in reliability‐critical systems such as autonomous driving systems. How to quickly reveal these faults in real‐world datasets that LLMs could face is important but challenging. The major reason is that the ground truth is necessary but the data labeling process is heavy considering the time and human effort. To handle this problem, in the conventional deep learning testing field, test selection methods have been proposed for efficiently evaluating deep learning models by prioritizing faults. However, despite their importance, the usefulness of these methods on LLMs is unclear and underexplored. In this paper, we conduct the first empirical study to investigate the effectiveness of existing test selection methods for LLMs. We focus on classification tasks because most existing test selection methods target this setting and reliably estimating confidence scores for variable‐length outputs in generative tasks remains challenging. Experimental results on four different tasks (including both code tasks and natural language processing tasks) and four LLMs (e.g., LLaMA3 and GPT‐4) demonstrated that simple methods such as Margin perform well on LLMs, but there is still a big room for improvement. Based on the study, we further propose MuCS, a prompt Mutation‐based prediction Confidence Smoothing framework to boost the test selection capability for LLMs specifically on classification tasks. Concretely, multiple prompt mutation techniques have been proposed to help collect diverse outputs for confidence smoothing. The results show that our proposed framework significantly enhances existing methods with test relative coverage improvement by up to 70.53%. Lili Quan 0001, Maxime Cordy, Yuheng Huang 0004, Lei Ma 0003, Xiaohong Li 0001 |
J. Softw. Evol. Process. | 4 |
| 2025 | MUPPAAL: Efficient Elimination and Reduction of Useless Mutants in Real-Time Model-Based SystemsabstractABSTRACT To assess test quality, mutation testing (MT) creates mutants by injecting artificial faults into the system and evaluates the ability of tests to distinguish these mutants. Tests distinguishing more mutants have also been proven empirically to detect more real faults. MT has been applied to many domains. We focus on MT for timed safety‐critical systems modelled as Timed Automata (TA). While powerful, MT usually yields equivalent and duplicate mutants, the former having the same behaviour as the original system and the latter other mutants. Such useless mutants bring no value, waste execution time and can be difficult to detect. We integrate useless mutant detection and removal strategies in our mutation framework MUPPAAL. MUPPAAL leverages existing equivalence‐avoiding mutation operators and focuses on detecting mutant duplicates using a scalable bisimulation algorithm and a fast approximate one based on biased simulation. We also demonstrate how to design an operator that reduces the occurrence of mutant duplicates. We evaluate MUPPAAL on six systems, demonstrating that (1) mutant duplicates account for up to 32% of all generated mutants, (2) our bisimulation approach scales effectively with these systems and (3) biased simulations further enhance performance. Our heuristic is 10 times faster than bisimulation and limits the exploration to two times the number of exact duplicates compared to up to 10 times for the baseline. Jaime Cuartas, David Cortés Sáenz, Joan S. Betancourt, Jesús Aranda, Maxime Cordy, James Jerson Ortiz, Gilles Perrouin, Pierre-Yves Schobbens |
Softw. Test. Verification Reliab. | 5 |
| 2025 | Assessing the Robustness of Test Selection Methods for Deep Neural NetworksabstractRegularly testing deep learning-powered systems on newly collected data is critical to ensure their reliability, robustness, and efficacy in real-world applications. This process is demanding due to the significant time and human effort required for labeling new data. While test selection methods alleviate manual labor by labeling and evaluating only a subset of data while meeting testing criteria, we observe that such methods with reported promising results are simply evaluated, e.g., testing on original test data. The question arises: are they always reliable? In this paper, we explore when and to what extent test selection methods fail. First, we identify potential pitfalls of 11 selection methods based on their construction. Second, we conduct a study to empirically confirm the existence of these pitfalls. Furthermore, we demonstrate how pitfalls can break the reliability of these methods. Concretely, methods for fault detection suffer from data that are: 1) correctly classified but uncertain, or 2) misclassified but confident. Remarkably, the test relative coverage achieved by such methods drops by up to 86.85%. Besides, methods for performance estimation are sensitive to the choice of intermediate-layer output. The effectiveness of such methods can be even worse than random selection when using an inappropriate layer. Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Wei Ma 0014, Mike Papadakis, Lei Ma 0003, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2024 | How Realistic Is Your Synthetic Data? Constraining Deep Generative Models for Tabular DataabstractDeep Generative Models (DGMs) have been shown to be powerful tools for generating tabular data, as they have been increasingly able to capture the complex distributions that characterize them. However, to generate realistic synthetic data, it is often not enough to have a good approximation of their distribution, as it also requires compliance with constraints that encode essential background knowledge on the problem at hand. In this paper, we address this limitation and show how DGMs for tabular data can be transformed into Constrained Deep Generative Models (C-DGMs), whose generated samples are guaranteed to be compliant with the given constraints. This is achieved by automatically parsing the constraints and transforming them into a Constraint Layer (CL) seamlessly integrated with the DGM. Our extensive experimental analysis with various DGMs and tasks reveals that standard DGMs often violate constraints, some exceeding 95% non-compliance, while their corresponding C-DGMs are never non-compliant. Then, we quantitatively demonstrate that, at training time, C-DGMs are able to exploit the background knowledge expressed by the constraints to outperform their standard counterparts with up to 4.5% improvement in utility and detection. Further, we show how our CL does not necessarily need to be integrated at training time, as it can be also used as a guardrail at inference time, still producing some improvements in the overall performance of the models. Finally, we show that our CL does not hinder the sample generation time of the models. Mihaela Catalina Stoian, Salijona Dyrmishi, Maxime Cordy, Thomas Lukasiewicz, Eleonora Giunchiglia |
ICLR | 3 |
| 2024 | SpecBCFuzz: Fuzzing LTL Solvers with Boundary ConditionsabstractLTL solvers check the satisfiability of Linear-time Temporal Logic (LTL) formulas and are widely used for verifying and testing critical software systems. Thus, potential bugs in the solvers' implementations can have a significant impact. We present SpecBCFuzz, a fuzzing method for finding bugs in LTL solvers, that is guided by boundary conditions (BCs), corner cases whose (un)satisfiability depends on rare traces. SpecBCFuzz implements a search-based algorithm that fuzzes LTL formulas giving relevance to BCs. It integrates syntactic and semantic similarity metrics to explore the vicinity of the seeded formulas with BCs. We evaluate SpecBCFuzz on 21 different configurations (including the latest and past releases) of four mature and state-of-the-art LTL solvers (NuSMV, Black, Aalta, and PLTL) that implement a diverse set of satisfiability algorithms. SpecBCFuzz produces 368,716 bug-triggering formulas, detecting bugs in 18 out of the 21 solvers' configurations we study. Overall, SpecBCFuzz reveals: soundness issues (wrong answers given by a solver) in Aalta and PLTL; crashes, e.g., segmentation faults, in NuSMV, Black and Aalta; flaky behaviors (different responses across re-runs of the solver on the same formula) in NuSMV and Aalta; performance bugs (large time performance degradation between successive versions of the solver on the same formula) in Black, Aalta and PLTL; and no bug in NuSMV BDD (all versions), suggesting that the latter is currently the most robust solver. Renzo Degiovanni, Maxime Cordy, Nazareno Aguirre, Yves Le Traon, Mike Papadakis |
ICSE | 3 |
| 2024 | The Importance of Accounting for Execution Failures when Predicting Test FlakinessabstractFlaky tests are tests that pass and fail on different executions of the same version of a program under test. They waste valuable developer time by making developers investigate false alerts (flaky test failures). To deal with this issue, many prediction methods have been proposed. However, the utility of these methods remains unclear since they are typically evaluated based on single-release data, ignoring that in many cases tests that fail flakily in one release also correctly fail (indicating the presence of bugs) in some other, meaning that it is possible for subsequent correctly-failing cases to pass unnoticed. In this paper, we show that this situation is prevalent and can raise significant concerns for both researchers and practitioners. In particular, we show that flaky tests, tests that exhibit flaky behaviour at some point in time, have a strong fault-revealing capability, i.e., they reveal more than 1/3 of all encountered regression faults. We also show that 76.2%, of all test executions that reveal faults in the codebase under test are made by tests that are classified as flaky by existing prediction methods. Overall, our findings motivate the need for future research to focus on predicting flaky test executions instead of flaky tests. Guillaume Haben, Sarra Habchi, John Micco, Mark Harman, Mike Papadakis, Maxime Cordy, Yves Le Traon |
ASE | 6 |
| 2024 | Constrained Adaptive Attack: Effective Adversarial Attack Against Deep Neural Networks for Tabular DataabstractState-of-the-art deep learning models for tabular data have recently achieved acceptable performance to be deployed in industrial settings. However, the robustness of these models remains scarcely explored. Contrary to computer vision, there are no effective attacks to properly evaluate the adversarial robustness of deep tabular models due to intrinsic properties of tabular data, such as categorical features, immutability, and feature relationship constraints. To fill this gap, we first propose CAPGD, a gradient attack that overcomes the failures of existing gradient attacks with adaptive mechanisms. This new attack does not require parameter tuning and further degrades the accuracy, up to 81\% points compared to the previous gradient attacks. Second, we design CAA, an efficient evasion attack that combines our CAPGD attack and MOEVA, the best search-based attack. We demonstrate the effectiveness of our attacks on five architectures and four critical use cases. Our empirical study demonstrates that CAA outperforms all existing attacks in 17 over the 20 settings, and leads to a drop in the accuracy by up to 96.1\% points and 21.9\% points compared to CAPGD and MOEVA respectively while being up to five times faster than MOEVA. Given the effectiveness and efficiency of our new attacks, we argue that they should become the minimal test for any new defense or robust architectures in tabular machine learning. Thibault Simonetto, Salah Ghamizi, Maxime Cordy |
NeurIPS | 3 |
| 2024 | TabularBench: Benchmarking Adversarial Robustness for Tabular Deep Learning in Real-world Use-casesabstractWhile adversarial robustness in computer vision is a mature research field, fewer researchers have tackled the evasion attacks against tabular deep learning, and even fewer investigated robustification mechanisms and reliable defenses. We hypothesize that this lag in the research on tabular adversarial attacks is in part due to the lack of standardized benchmarks. To fill this gap, we propose TabularBench, the first comprehensive benchmark of robustness of tabular deep learning classification models. We evaluated adversarial robustness with CAA, an ensemble of gradient and search attacks which was recently demonstrated as the most effective attack against a tabular model. In addition to our open benchmark https://github.com/serval-uni-lu/tabularbench where we welcome submissions of new models and defenses, we implement 7 robustification mechanisms inspired by state-of-the-art defenses in computer vision and propose the largest benchmark of robust tabular deep learning over 200 models across five critical scenarios in finance, healthcare and security. We curated real datasets for each use case, augmented with hundreds of thousands of realistic synthetic inputs, and trained and assessed our models with and without data augmentations. We open-source our library that provides API access to all our pre-trained robust tabular models, and the largest datasets of real and synthetic tabular inputs. Finally, we analyze the impact of various defenses on the robustness and provide actionable insights to design new defenses and robustification mechanisms. Thibault Simonetto, Salah Ghamizi, Maxime Cordy |
NeurIPS | 3 |
| 2024 | Towards Exploring the Limitations of Test Selection Techniques on Graph Neural Networks: An Empirical StudyabstractAbstract Graph Neural Networks (GNNs) have gained prominence in various domains, such as social network analysis, recommendation systems, and drug discovery, due to their ability to model complex relationships in graph-structured data. GNNs can exhibit incorrect behavior, resulting in severe consequences. Therefore, testing is necessary and pivotal. However, labeling all test inputs for GNNs can be prohibitively costly and time-consuming, especially when dealing with large and complex graphs. In response to these challenges, test selection has emerged as a strategic approach to alleviate labeling expenses. The objective of test selection is to select a subset of tests from the complete test set. While various test selection techniques have been proposed for traditional deep neural networks (DNNs), their adaptation to GNNs presents unique challenges due to the distinctions between DNN and GNN test data. Specifically, DNN test inputs are independent of each other, whereas GNN test inputs (nodes) exhibit intricate interdependencies. Therefore, it remains unclear whether DNN test selection approaches can perform effectively on GNNs. To fill the gap, we conduct an empirical study that systematically evaluates the effectiveness of various test selection methods in the context of GNNs, focusing on three critical aspects: 1) Misclassification detection : selecting test inputs that are more likely to be misclassified; 2) Accuracy estimation : selecting a small set of tests to precisely estimate the accuracy of the whole testing set; 3) Performance enhancement : selecting retraining inputs to improve the GNN accuracy. Our empirical study encompasses 7 graph datasets and 8 GNN models, evaluating 22 test selection approaches. Our study includes not only node classification datasets but also graph classification datasets. Our findings reveal that: 1) In GNN misclassification detection, confidence-based test selection methods, which perform well in DNNs, do not demonstrate the same level of effectiveness; 2) In terms of GNN accuracy estimation, clustering-based methods, while consistently performing better than random selection, provide only slight improvements; 3) Regarding selecting inputs for GNN performance improvement, test selection methods, such as confidence-based and clustering-based test selection methods, demonstrate only slight effectiveness; 4) Concerning performance enhancement, node importance-based test selection methods are not suitable, and in many cases, they even perform worse than random selection. Xueqi Dang, Wei Ma 0014, Yuejun Guo 0001, Mike Papadakis, Maxime Cordy, Yves Le Traon |
Empir. Softw. Eng. | 7 |
| 2024 | On the effectiveness of hybrid pooling in mixup-based graph learning for language processing
Zeming Dong, Zhenya Zhang 0001, Yuejun Guo 0001, Maxime Cordy, Mike Papadakis, Yves Le Traon, Jianjun Zhao 0001 |
J. Syst. Softw. | 5 |
| 2024 | KAPE: kNN-based Performance Testing for Deep Code SearchabstractCode search is a common yet important activity of software developers. An efficient code search model can largely facilitate the development process and improve the programming quality. Given the superb performance of learning the contextual representations, deep learning models, especially pre-trained language models, have been widely explored for the code search task. However, studies mainly focus on proposing new architectures for ever-better performance on designed test sets but ignore the performance on unseen test data where only natural language queries are available. The same problem in other domains, e.g., CV and NLP, is usually solved by test input selection that uses a subset of the unseen set to reduce the labeling effort. However, approaches from other domains are not directly applicable and still require labeling effort. In this article, we propose the k NN-b a sed p erformance t e sting ( KAPE ) to efficiently solve the problem without manually matching code snippets to test queries. The main idea is to use semantically similar training data to perform the evaluation. Extensive experiments on six programming language datasets, three state-of-the-art pre-trained models, and seven baseline methods demonstrate that KAPE can effectively assess the model performance (e.g., CodeBERT achieves MRR 0.5795 on JavaScript) with a slight difference (e.g., 0.0261). Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Mike Papadakis, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2024 | Test Optimization in DNN Testing: A SurveyabstractThis article presents a comprehensive survey on test optimization in deep neural network (DNN) testing. Here, test optimization refers to testing with low data labeling effort. We analyzed 90 papers, including 43 from the software engineering (SE) community, 32 from the machine learning (ML) community, and 15 from other communities. Our study: (i) unifies the problems as well as terminologies associated with low-labeling cost testing, (ii) compares the distinct focal points of SE and ML communities, and (iii) reveals the pitfalls in existing literature. Furthermore, we highlight the research opportunities in this domain. Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Lei Ma 0003, Mike Papadakis, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2024 | LaF: Labeling-free Model Selection for Automated Deep Neural Network ReusingabstractApplying deep learning (DL) to science is a new trend in recent years, which leads DL engineering to become an important problem. Although training data preparation, model architecture design, and model training are the normal processes to build DL models, all of them are complex and costly. Therefore, reusing the open-sourced pre-trained model is a practical way to bypass this hurdle for developers. Given a specific task, developers can collect massive pre-trained deep neural networks from public sources for reusing. However, testing the performance (e.g., accuracy and robustness) of multiple deep neural networks (DNNs) and recommending which model should be used is challenging regarding the scarcity of labeled data and the demand for domain expertise. In this article, we propose a labeling-free (LaF) model selection approach to overcome the limitations of labeling efforts for automated model reusing. The main idea is to statistically learn a Bayesian model to infer the models’ specialty only based on predicted labels. We evaluate LaF using nine benchmark datasets, including image, text, and source code, and 165 DNNs, considering both the accuracy and robustness of models. The experimental results demonstrate that LaF outperforms the baseline methods by up to 0.74 and 0.53 on Spearman’s correlation and Kendall’s τ, respectively. Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Mike Papadakis, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2024 | Active Code Learning: Benchmarking Sample-Efficient Training of Code ModelsabstractThe costly human effort required to prepare the training data of machine learning (ML) models hinders their practical development and usage in software engineering (ML4Code), especially for those with limited budgets. Therefore, efficiently training models of code with less human effort has become an emergent problem. Active learning is such a technique to address this issue that allows developers to train a model with reduced data while producing models with desired performance, which has been well studied in computer vision and natural language processing domains. Unfortunately, there is no such work that explores the effectiveness of active learning for code models. In this paper, we bridge this gap by building the first benchmark to study this critical problem - active code learning. Specifically, we collect 11 acquisition functions (which are used for data selection in active learning) from existing works and adapt them for code-related tasks. Then, we conduct an empirical study to check whether these acquisition functions maintain performance for code data. The results demonstrate that feature selection highly affects active learning and using output vectors to select data is the best choice. For the code summarization task, active code learning is ineffective which produces models with over a 29.64% gap compared to the expected performance. Furthermore, we explore future directions of active code learning with an exploratory study. We propose to replace distance calculation methods with evaluation metrics and find a correlation between these evaluation-based distance methods and the performance of code models. Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Lei Ma 0003, Mike Papadakis, Yves Le Traon |
IEEE Trans. Software Eng. | 4 |
| 2023 | How do humans perceive adversarial text? A reality check on the validity and naturalness of word-based adversarial attacksabstractNatural Language Processing (NLP) models based on Machine Learning (ML) are susceptible to adversarial attacks -malicious algorithms that imperceptibly modify input text to force models into making incorrect predictions.However, evaluations of these attacks ignore the property of imperceptibility or study it under limited settings.This entails that adversarial perturbations would not pass any human quality gate and do not represent real threats to human-checked NLP systems.To bypass this limitation and enable proper assessment (and later, improvement) of NLP model robustness, we have surveyed 378 human participants about the perceptibility of text adversarial examples produced by state-of-the-art methods.Our results underline that existing text attacks are impractical in real-world scenarios where humans are involved.This contrasts with previous smaller-scale human studies, which reported overly optimistic conclusions regarding attack success.Through our work, we hope to position human perceptibility as a first-class success criterion for text attacks, and provide guidance for research to build effective attack algorithms and, in turn, design appropriate defence mechanisms. Salijona Dyrmishi, Salah Ghamizi, Maxime Cordy |
ACL (1) | 3 |
| 2023 | Towards Understanding Model Quantization for Reliable Deep Neural Network DeploymentabstractDeep Neural Networks (DNNs) have gained considerable attention in the past decades due to their astounding performance in different applications, such as natural language modeling, self-driving assistance, and source code understanding. With rapid exploration, more and more complex DNN architectures have been proposed along with huge pre-trained model parameters. A common way to use such DNN models in user-friendly devices (e.g., mobile phones) is to perform model compression before deployment. However, recent research has demonstrated that model compression, e.g., model quantization, yields accuracy degradation as well as output disagreements when tested on unseen data. Since the unseen data always include distribution shifts and often appear in the wild, the quality and reliability of models after quantization are not ensured. In this paper, we conduct a comprehensive study to characterize and help users understand the behaviors of quantization models. Our study considers four datasets spanning from image to text, eight DNN architectures including both feed-forward neural networks and recurrent neural networks, and 42 shifted sets with both synthetic and natural distribution shifts. The results reveal that 1) data with distribution shifts lead to more disagreements than without. 2) Quantization-aware training can produce more stable models than standard, adversarial, and Mixup training. 3) Disagreements often have closer top-1 and top-2 output probabilities, and Margin is a better indicator than other uncertainty metrics to distinguish disagreements. 4) Retraining the model with disagreements has limited efficiency in removing disagreements. We release our code and models as a new benchmark for further study of model quantization. Yuejun Guo 0001, Maxime Cordy, Xiaofei Xie, Wei Ma 0014, Mike Papadakis, Yves Le Traon |
CAIN | 3 |
| 2023 | ACoRe: Automated Goal-Conflict ResolutionabstractAbstract System goals are the statements that, in the context of software requirements specification, capture how the software should behave. Many times, the understanding of stakeholders on what the system should do, as captured in the goals, can lead to different problems, from clearly contradicting goals, to more subtle situations in which the satisfaction of some goals inhibits the satisfaction of others. These latter issues, calledgoal divergences, are the subject ofgoal conflict analysis, which consists of identifying, assessing, and resolving divergences, as part of a more general activity known as goal refinement. While there exist techniques that, when requirements are expressed formally, can automatically identify and assess goal conflicts, there is currently no automated approach to support engineers inresolvingidentified divergences. In this paper, we presentACoRe, the first approach that automatically proposes potential resolutions to goal conflicts, in requirements specifications formally captured using linear-time temporal logic.ACoResystematically explores syntactic modifications of the conflicting specifications, aiming at obtaining resolutions that disable previously identified conflicts, while preserving specification consistency.ACoReintegrates modern multi-objective search algorithms (in particular, NSGA-III, WBGA, and AMOSA) to produce resolutions that maintain coherence with the original conflicting specification, by searching for specifications that are eithersyntacticallyorsemanticallysimilar to the original specification. We assessACoReon 25 requirements specifications taken from the literature. We show thatACoRecan successfully produce various conflict resolutions for each of the analyzed case studies, including resolutions that resemble specification repairs manually provided as part of conflict analyses. Renzo Degiovanni, Matías Brizzio, Maxime Cordy, Nazareno Aguirre, Yves Le Traon, Mike Papadakis |
FASE | 4 |
| 2023 | Automated Repair of Unrealisable LTL Specifications Guided by Model CountingabstractThe reactive synthesis problem consists of automatically producing correct-by-construction operational models of systems from high-level formal specifications of their behaviours. However, specifications are often unrealisable, meaning that no system can be synthesised from the specification. To deal with this problem, we present AuRUS, a search-based approach to repair unrealisable Linear-Time Temporal Logic (LTL) specifications. AuRUS aims at generating solutions that are similar to the original specifications by using the notions of syntactic and semantic similarities. Intuitively, the syntactic similarity measures the text similarity between the specifications, while the semantic similarity measures the number of behaviours preserved/removed by the candidate repair. We propose a new heuristic based on model counting to approximate semantic similarity. We empirically assess AuRUS on many unrealisable specifications taken from different benchmarks and show that it can successfully repair all of them. Also, compared to related techniques, AuRUS can produce many unique solutions while showing more scalability. Matías Brizzio, Maxime Cordy, Mike Papadakis, César Sánchez 0001, Nazareno Aguirre, Renzo Degiovanni |
GECCO | 2 |
| 2023 | GAT: Guided Adversarial Training with Pareto-optimal Auxiliary TasksabstractWhile leveraging additional training data is well established to improve adversarial robustness, it incurs the unavoidable cost of data collection and the heavy computation to train models. To mitigate the costs, we propose *Guided Adversarial Training * (GAT), a novel adversarial training technique that exploits auxiliary tasks under a limited set of training data. Our approach extends single-task models into multi-task models during the min-max optimization of adversarial training, and drives the loss optimization with a regularization of the gradient curvature across multiple tasks. GAT leverages two types of auxiliary tasks: self-supervised tasks, where the labels are generated automatically, and domain-knowledge tasks, where human experts provide additional labels. Experimentally, under limited data, GAT increases the robust accuracy on CIFAR-10 up to four times (from 11% to 42% robust accuracy) and the robust AUC of CheXpert medical imaging dataset from 50% to 83%. On the full CIFAR-10 dataset, GAT outperforms eight state-of-the-art adversarial training strategies. Our large study across five datasets and six tasks demonstrates that task augmentation is an efficient alternative to data augmentation, and can be key to achieving both clean and robust performances. Salah Ghamizi, Jingfeng Zhang, Maxime Cordy, Mike Papadakis, Masashi Sugiyama, Yves Le Traon |
ICML | 3 |
| 2023 | Aries: Efficient Testing of Deep Neural Networks via Labeling-Free Accuracy EstimationabstractDeep learning (DL) plays a more and more important role in our daily life due to its competitive performance in industrial application domains. As the core of DL-enabled systems, deep neural networks (DNNs) need to be carefully evaluated to ensure the produced models match the expected requirements. In practice, the de facto standard to assess the quality of DNNs in the industry is to check their performance (accuracy) on a collected set of labeled test data. However, preparing such labeled data is often not easy partly because of the huge labeling effort, i.e., data labeling is labor-intensive, especially with the massive new incoming unlabeled data every day. Recent studies show that test selection for DNN is a promising direction that tackles this issue by selecting minimal representative data to label and using these data to assess the model. However, it still requires human effort and cannot be automatic. In this paper, we propose a novel technique, named Aries, that can estimate the performance of DNNs on new unlabeled data using only the information obtained from the original test data. The key insight behind our technique is that the model should have similar prediction accuracy on the data which have similar distances to the decision boundary. We performed a large-scale evaluation of our technique on two famous datasets, CIFAR-10 and Tiny-ImageNet, four widely studied DNN models including ResNetl0l and DenseNetl21, and 13 types of data transformation methods. Results show that the estimated accuracy by Aries is only 0.03% - 2.60% off the true accuracy. Besides, Aries also outperforms the state-of-the-art labeling-free methods in 50 out of 52 cases and selection-labeling-based methods in 96 out of 128 cases. Yuejun Guo 0001, Xiaofei Xie, Maxime Cordy, Mike Papadakis, Lei Ma 0003, Yves Le Traon |
ICSE | 4 |
| 2023 | Enabling Efficient Assertion InferenceabstractAssertion inference techniques aim at automatically inferring sets of program assertions that capture the exhibited software behavior, often by generating and filtering assertions through dynamic test executions and mutation testing. Although powerful, such techniques are computationally expensive due to the large number of mutants that require execution. In this study, we introduce the notion of Assertion Inferring Mutants, and demonstrate that these mutants are sufficient for assertion inference and correspond to a small subset (12.95%) of the entire mutant set. Moreover, these mutants are significantly different (71.59%) from Subsuming Mutants that are frequently cited by mutation testing literature. We also show that Assertion Inferring Mutants can be statically approximated via a learning-based method. Given the widespread adoption of encoder-decoder architecture for prediction tasks, we demonstrate that it predicts Assertion Inferring Mutants with 0.79 Precision and 0.49 Recall. Its evaluation on 46 projects showcases that it enables a comparable inference capability (missing only 12.49% assertions) with a complete mutation analysis, while significantly reducing the execution cost (achieving 46.29 times faster inference). Moreover, it enables assertion inference techniques to scale on subjects where complete mutation testing is prohibitively expensive and other mutant selection strategies do not lead to an acceptable assertion inference. Aayush Garg, Renzo Degiovanni, Facundo Molina, Maxime Cordy, Nazareno Aguirre, Mike Papadakis, Yves Le Traon |
ISSRE | 4 |
| 2023 | MUTEN: Mutant-Based Ensembles for Boosting Gradient-Based Adversarial AttackabstractMutation testing (MT) for deep learning (DL) has gained huge attention in the past few years. However, how MT can really help DL is still unclear. In this paper, we introduce one promising direction for the usage of mutants. Specifically, since mutants can be seen as one kind of ensemble model and ensemble model can be used to boost the adversarial attack, we propose MUTEN, which applies the attack on mutants to improve the success rate of well-known attacks against gradient-masking models. Experimental results on MNIST, SVHN, and CIFAR-10 show that MUTEN can increase the success rate of four attacks by up to 45%. Furthermore, experiments on four defense approaches, bit-depth reduction, JPEG compression, Defensive distillation, and Label smoothing, demonstrate that MUTEN can break the defense models effectively by enhancing the attacks with the success rate of up to 96%. Yuejun Guo 0001, Maxime Cordy, Mike Papadakis, Yves Le Traon |
ASE | 3 |
| 2023 | Towards Strengthening Formal Specifications with Mutation Model CheckingabstractWe propose mutation model checking as an approach to strengthen formal specifications used for model checking. Inspired by mutation testing, our approach concludes that specifications are not strong enough if they fail to detect faults in purposely mutated models. Our preliminary experiments on two case studies confirm the relevance of the problem: their specification can only detect 40% and 60% of randomly generated mutants. As a result, we propose a framework to strengthen the original specification, such that the original model satisfies the strengthened specification but the mutants do not. Maxime Cordy, Sami Lazreg, Axel Legay, Pierre-Yves Schobbens |
ESEC/SIGSOFT FSE | 1 |
| 2023 | On The Empirical Effectiveness of Unrealistic Adversarial Hardening Against Realistic Adversarial AttacksabstractWhile the literature on security attacks and defenses of Machine Learning (ML) systems mostly focuses on unrealistic adversarial examples, recent research has raised concern about the under-explored field of realistic adversarial attacks and their implications on the robustness of real-world systems. Our paper paves the way for a better understanding of adversarial robustness against realistic attacks and makes two major contributions. First, we conduct a study on three real-world use cases (text classification, botnet detection, malware detection) and seven datasets in order to evaluate whether unrealistic adversarial examples can be used to protect models against realistic examples. Our results reveal discrepancies across the use cases, where unrealistic examples can either be as effective as the realistic ones or may offer only limited improvement. Second, to explain these results, we analyze the latent representation of the adversarial examples generated with realistic and unrealistic attacks. We shed light on the patterns that discriminate which unrealistic examples can be used for effective hardening. We release our code, datasets and models to support future research in exploring how to reduce the gap between unrealistic and realistic adversarial attacks. Salijona Dyrmishi, Salah Ghamizi, Thibault Simonetto, Yves Le Traon, Maxime Cordy |
SP | 5 |
| 2023 | MixCode: Enhancing Code Classification by Mixup-Based Data AugmentationabstractInspired by the great success of Deep Neural Networks (DNNs) in natural language processing (NLP), DNNs have been increasingly applied in source code analysis and attracted significant attention from the software engineering community. Due to its data-driven nature, a DNN model requires massive and high-quality labeled training data to achieve expert-level performance. Collecting such data is often not hard, but the labeling process is notoriously laborious. The task of DNN-based code analysis even worsens the situation because source code labeling also demands sophisticated expertise. Data augmentation has been a popular approach to supplement training data in domains such as computer vision and NLP. However, existing data augmentation approaches in code analysis adopt simple methods, such as data transformation and adversarial example generation, thus bringing limited performance superiority. In this paper, we propose a data augmentation approach MixCode that aims to effectively supplement valid training data, inspired by the recent advance named Mixup in computer vision. Specifically, we first utilize multiple code refactoring methods to generate transformed code that holds consistent labels with the original data. Then, we adapt the Mixup technique to mix the original code with the transformed code to augment the training data. We evaluate MixCode on two programming languages (Java and Python), two code tasks (problem classification and bug detection), four benchmark datasets (JAVA250, Python800, CodRep1, and Refactory), and seven model architectures (including two pretrained models CodeBERT and GraphCodeBERT). Experimental results demonstrate that MixCode outperforms the baseline data augmentation approach by up to 6.24% in accuracy and 26.06% in robustness. Zeming Dong, Yuejun Guo 0001, Maxime Cordy, Mike Papadakis, Zhenya Zhang 0001, Yves Le Traon, Jianjun Zhao 0001 |
SANER | 4 |
| 2023 | DRE: density-based data selection with entropy for adversarial-robust deep learning modelsabstractAbstract Active learning helps software developers reduce the labeling cost when building high-quality machine learning models. A core component of active learning is the acquisition function that determines which data should be selected to annotate.State-of-the-art (SOTA) acquisition functions focus on clean performance (e.g. accuracy) but disregard robustness (an important quality property), leading to fragile models with negligible robustness (less than 0.20%). In this paper, we first propose to integrate adversarial training into active learning (adversarial-robust active learning, ARAL) to produce robust models. Our empirical study on 11 acquisition functions and 15105 trained deep neural networks (DNNs) shows that ARAL can produce models with robustness ranging from 2.35% to 63.85%. Our study also reveals, however, that the acquisition functions that perform well on accuracy are worse than random sampling when it comes to robustness. Via examining the reasons behind this, we devise the density-based robust sampling with entropy (DRE) to target both clean performance and robustness. The core idea of DRE is to maintain a balance between selected data and the entire set based on the entropy density distribution. DRE outperforms SOTA functions in terms of robustness by up to 24.40%, while remaining competitive on accuracy. Additionally, the in-depth evaluation shows that DRE is applicable as a test selection metric for model retraining and stands out from all compared functions by up to 8.21% robustness. Yuejun Guo 0001, Maxime Cordy, Michail Papadakis, Yves Le Traon |
Neural Comput. Appl. | 3 |
| 2023 | BURST: Benchmarking uniform random sampling techniques
Mathieu Acher, Gilles Perrouin, Maxime Cordy |
Sci. Comput. Program. | 3 |
| 2023 | iBiR: Bug-report-driven Fault InjectionabstractMuch research on software engineering relies on experimental studies based on fault injection. Fault injection, however, is not often relevant to emulate real-world software faults since it “blindly” injects large numbers of faults. It remains indeed challenging to inject few but realistic faults that target a particular functionality in a program. In this work, we introduce iBiR , a fault injection tool that addresses this challenge by exploring change patterns associated to user-reported faults. To inject realistic faults, we create mutants by re-targeting a bug-report-driven automated program repair system, i.e., reversing its code transformation templates. iBiR is further appealing in practice since it requires deep knowledge of neither code nor tests, just of the program’s relevant bug reports. Thus, our approach focuses the fault injection on the feature targeted by the bug report. We assess iBiR by considering the Defects4J dataset. Experimental results show that our approach outperforms the fault injection performed by traditional mutation testing in terms of semantic similarity with the original bug, when applied at either system or class levels of granularity, and provides better, statistically significant estimations of test effectiveness (fault detection). Additionally, when injecting 100 faults, iBiR injects faults that couple with the real ones in around 36% of the cases, while mutation testing achieves less than 4%. Ahmed Khanfir, Anil Koyuncu, Mike Papadakis, Maxime Cordy, Tegawendé F. Bissyandé, Jacques Klein, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2022 | Adversarial Robustness in Multi-Task Learning: Promises and IllusionsabstractVulnerability to adversarial attacks is a well-known weakness of Deep Neural networks. While most of the studies focus on single-task neural networks with computer vision datasets, very little research has considered complex multi-task models that are common in real applications. In this paper, we evaluate the design choices that impact the robustness of multi-task deep learning networks. We provide evidence that blindly adding auxiliary tasks, or weighing the tasks provides a false sense of robustness. Thereby, we tone down the claim made by previous research and study the different factors which may affect robustness. In particular, we show that the choice of the task to incorporate in the loss function are important factors that can be leveraged to yield more robust models. We provide the appendix, all our algorithms, models, and open source-code at https://github.com/yamizi/taskaugment Salah Ghamizi, Maxime Cordy, Mike Papadakis, Yves Le Traon |
AAAI | 2 |
| 2022 | Robust active learning: sample-efficient training of robust deep learning modelsabstractActive learning is an established technique to reduce the labeling cost for building high-quality machine learning models. However, state-of-the-art approaches focus on maximizing the clean performance (e.g. accuracy) but disregarding robustness. In this work, we propose Robust Active Learning, an active learning process that integrates adversarial training, the most established method to produce robust models. First, we conduct an empirical study to evaluate the effectiveness of existing approaches and uncover the characteristics of data. Then, we propose a novel approach, density-based robust sampling with entropy (DRE), to target both clean performance and robustness. Our experiments are conducted on 11 acquisition functions, 4 datasets, 6 DNN architectures, and 15105 trained DNNs. Yuejun Guo 0001, Maxime Cordy, Mike Papadakis, Yves Le Traon |
CAIN | 3 |
| 2022 | Influence-driven data poisoning in graph-based semi-supervised classifiersabstractGraph-based Semi-Supervised Learning (GSSL) is a practical solution to learn from a limited amount of labelled data together with a vast amount of unlabelled data. However, due to their reliance on the known labels to infer the unknown labels, these algorithms are sensitive to data quality. It is therefore essential to study the potential threats related to the labelled data, more specifically, label poisoning. In this paper, we propose a novel data poisoning method which efficiently approximates the result of label inference to identify the inputs which, if poisoned, would produce the highest number of incorrectly inferred labels. We extensively evaluate our approach on three classification problems under 24 different experimental settings each. Compared to the state of the art, our influence-driven attack produces an average increase of error rate 50% higher, while being faster by multiple orders of magnitude. Moreover, our method can inform engineers of inputs that deserve investigation (relabelling them) before training the learning model. We show that relabelling one-third of the poisoned inputs (selected based on their influence) reduces the poisoning effect by 50%. Adriano Franci, Maxime Cordy, Martin Gubri, Mike Papadakis, Yves Le Traon |
CAIN | 2 |
| 2022 | LGV: Boosting Adversarial Example Transferability from Large Geometric Vicinity
Martin Gubri, Maxime Cordy, Mike Papadakis, Yves Le Traon, Koushik Sen |
ECCV (4) | 2 |
| 2022 | FlakiMe: Laboratory-Controlled Test Flakiness Impact AssessmentabstractMuch research on software testing makes an implicit assumption that test failures are deterministic such that they always witness the presence of the same defects. However, this assumption is not always true because some test failures are due to so-called flaky tests, i.e., tests with non-deterministic outcomes. To help testing researchers better investigate flakiness, we introduce a test flakiness assessment and experimentation platform, called FlakiMe. FlakiMe supports the seeding of a (controllable) degree of flakiness into the behaviour of a given test suite. Thereby, FlakiMe equips researchers with ways to investigate the impact of test flakiness on their techniques under laboratory-controlled conditions. To demonstrate the application of FlakiMe, we use it to assess the impact of flakiness on mutation testing and program repair (the PRAPR and ARJA methods). These results indicate that a 10% flakiness is sufficient to affect the mutation score, but the effect size is modest (2% - 5% ), while it reduces the number of patches produced for repair by 20% up to 100% of repair problems; a devastating impact on this application of testing. Our experiments with FlakiMe demonstrate that flakiness affects different testing applications in very different ways, thereby motivating the need for a laboratory-controllable flakiness impact assessment platform and approach such as FlakiMe. Maxime Cordy, Renaud Rwemalika, Adriano Franci, Mike Papadakis, Mark Harman |
ICSE | 1 |
| 2022 | What Made This Test Flake? Pinpointing Classes Responsible for Test FlakinessabstractFlaky tests are defined as tests that manifest non-deterministic behaviour by passing and failing intermittently for the same version of the code. These tests cripple continuous integration with false alerts that waste developers’ time and break their trust in regression testing. To mitigate the effects of flakiness, both researchers and industrial experts proposed strategies and tools to detect and isolate flaky tests. However, flaky tests are rarely fixed as developers struggle to localise and understand their causes. Additionally, developers working with large codebases often need to know the sources of non-determinism to preserve code quality, i.e., avoid introducing technical debt linked with non-deterministic behaviour, and to avoid introducing new flaky tests. To aid with these tasks, we propose re-targeting Fault Localisation techniques to the flaky component localisation problem, i.e., pinpointing program classes that cause the non-deterministic behaviour of flaky tests. In particular, we employ Spectrum-Based Fault Localisation (SBFL), a coverage-based fault localisation technique commonly adopted for its simplicity and effectiveness. We also utilise other data sources, such as change history and static code metrics, to further improve the localisation. Our results show that augmenting SBFL with change and code metrics ranks flaky classes in the top-1 and top-5 suggestions, in 26% and 47% of the cases. Overall, we successfully reduced the average number of classes inspected to locate the first flaky class to 19% of the total number of classes covered by flaky tests. Our results also show that localisation methods are effective in major flakiness categories, such as concurrency and asynchronous waits, indicating their general ability to identify flaky components. Sarra Habchi, Guillaume Haben, Jeongju Sohn, Adriano Franci, Mike Papadakis, Maxime Cordy, Yves Le Traon |
ICSME | 6 |
| 2022 | A Qualitative Study on the Sources, Impacts, and Mitigation Strategies of Flaky TestsabstractTest flakiness forms a major testing concern. Flaky tests manifest non-deterministic outcomes that cripple continu-ous integration and lead developers to investigate false alerts. Industrial reports indicate that on a large scale, the accrual of flaky tests breaks the trust in test suites and entails significant computational cost. To alleviate this, practitioners are constrained to identify flaky tests and investigate their impact. To shed light on such mitigation mechanisms, we interview 14 practitioners with the aim to identify (i) the sources of flakiness within the testing ecosystem, (ii) the impacts of flakiness, (iii) the measures adopted by practitioners when addressing flakiness, and (iv) the automation opportunities for these measures. Our analysis shows that, besides the tests and code, flakiness stems from interactions between the system components, the testing infrastructure, and external factors. We also highlight the impact of flakiness on testing practices and product quality and show that the adoption of guidelines together with a stable infrastructure are key measures in mitigating the problem. Sarra Habchi, Guillaume Haben, Mike Papadakis, Maxime Cordy, Yves Le Traon |
ICST | 4 |
| 2022 | A Unified Framework for Adversarial Attack and Defense in Constrained Feature SpaceabstractThe generation of feasible adversarial examples is necessary for properly assessing models that work in constrained feature space. However, it remains a challenging task to enforce constraints into attacks that were designed for computer vision. We propose a unified framework to generate feasible adversarial examples that satisfy given domain constraints. Our framework can handle both linear and non-linear constraints. We instantiate our framework into two algorithms: a gradient-based attack that introduces constraints in the loss function to maximize, and a multi-objective search algorithm that aims for misclassification, perturbation minimization, and constraint satisfaction. We show that our approach is effective in four different domains, with a success rate of up to 100%, where state-of-the-art attacks fail to generate a single feasible example. In addition to adversarial retraining, we propose to introduce engineered non-convex constraints to improve model adversarial robustness. We demonstrate that this new defense is as effective as adversarial retraining. Our framework forms the starting point for research on constrained adversarial attacks and provides relevant baselines and datasets that future research can exploit. Thibault Simonetto, Salijona Dyrmishi, Salah Ghamizi, Maxime Cordy, Yves Le Traon |
IJCAI | 4 |
| 2022 | Automated Repair of Security Errors in C Programs via Statistical Model Checking: A Proof of Concept
Khanh-Huu-The Dam, Fabien Duchene 0001, Thomas Given-Wilson, Maxime Cordy, Axel Legay |
ISoLA (1) | 4 |
| 2022 | Verification of Variability-Intensive Stochastic Systems with Statistical Model CheckingabstractAbstract We propose a simulation-based approach to verify Variability-Intensive Systems (VISs) with stochastic behaviour. Given an LTL formula and a model of the VIS behaviour, our method estimates the probability for each variant to satisfy the formula. This allows us to learn the products of the VIS for which the probability stands above a certain threshold. To achieve this, our method samples VIS executions from all variants at once and keeps track of the occurrence probability of these executions in any given variant. The efficiency of this algorithm relies on Algebraic Decision Diagram (ADD), a dedicated data structure that enables orthogonal treatment of variability, stochasticity and property satisfaction. We implemented our approach as an extension of the ProVeLines model checker. Our experiments validate that our method can produce accurate estimations of the probability for the variants to satisfy the given properties. Sami Lazreg, Maxime Cordy, Axel Legay |
ISoLA (3) | 2 |
| 2022 | GraphCode2Vec: Generic Code Embedding via Lexical and Program Dependence Analysesabstractpeer reviewed Wei Ma 0014, Ezekiel O. Soremekun, Jie Zhang 0050, Mike Papadakis, Maxime Cordy, Xiaofei Xie, Yves Le Traon |
MSR | 7 |
| 2022 | Efficient and transferable adversarial examples from bayesian neural networksabstractAn established way to improve the transferability of black-box evasion attacks is to craft the adversarial examples on an ensemble-based surrogate to increase diversity. We argue that transferability is fundamentally related to uncertainty. Based on a state-of-the-art Bayesian Deep Learning technique, we propose a new method to efficiently build a surrogate by sampling approximately from the posterior distribution of neural network weights, which represents the belief about the value of each parameter. Our extensive experiments on ImageNet, CIFAR-10 and MNIST show that our approach improves the success rates of four state-of-the-art attacks significantly (up to 83.2 percentage points), in both intra-architecture and inter-architecture transferability. On ImageNet, our approach can reach 94% of success rate while reducing training computations from 11.6 to 2.4 exaflops, compared to an ensemble of independently trained DNNs. Our vanilla surrogate achieves 87.5% of the time higher transferability than three test-time techniques designed for this purpose. Our work demonstrates that the way to train a surrogate has been overlooked, although it is an important element of transfer-based attacks. We are, therefore, the first to review the effectiveness of several training methods in increasing transferability. We provide new directions to better understand the transferability phenomenon and offer a simple but strong baseline for future work. Martin Gubri, Maxime Cordy, Mike Papadakis, Yves Le Traon, Koushik Sen |
UAI | 2 |
| 2022 | Static detection of equivalent mutants in real-time model-based mutation testingabstractAbstract Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that are equivalent to the original system model, making it impossible to generate test cases from them. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our empirical evaluation, based on a proof-of-concept implementation and a set of benchmarks from the literature, confirms the validity of our theory and demonstrates that in general our approach can avoid the generation of a significant amount of the equivalent mutants. Davide Basile 0001, Maurice H. ter Beek, Sami Lazreg, Maxime Cordy, Axel Legay |
Empir. Softw. Eng. | 4 |
| 2022 | Learning from what we know: How to perform vulnerability prediction using noisy historical dataabstractAbstract Vulnerability prediction refers to the problem of identifying system components that are most likely to be vulnerable. Typically, this problem is tackled by training binary classifiers on historical data. Unfortunately, recent research has shown that such approaches underperform due to the following two reasons: a) the imbalanced nature of the problem, and b) the inherently noisy historical data, i.e., most vulnerabilities are discovered much later than they are introduced. This misleads classifiers as they learn to recognize actual vulnerable components as non-vulnerable. To tackle these issues, we propose TROVON , a technique that learns from known vulnerable components rather than from vulnerable and non-vulnerable components, as typically performed. We perform this by contrasting the known vulnerable, and their respective fixed components. This way, TROVON manages to learn from the things we know, i.e., vulnerabilities, hence reducing the effects of noisy and unbalanced data. We evaluate TROVON by comparing it with existing techniques on three security-critical open source systems, i.e., Linux Kernel, OpenSSL, and Wireshark, with historical vulnerabilities that have been reported in the National Vulnerability Database (NVD). Our evaluation demonstrates that the prediction capability of TROVON significantly outperforms existing vulnerability prediction techniques such as Software Metrics , Imports , Function Calls , Text Mining , Devign , LSTM , and LSTM-RF with an improvement of 40.84% in Matthews Correlation Coefficient (MCC) score under Clean Training Data Settings , and an improvement of 35.52% under Realistic Training Data Settings . Aayush Garg, Renzo Degiovanni, Matthieu Jimenez, Maxime Cordy, Mike Papadakis, Yves Le Traon |
Empir. Softw. Eng. | 4 |
| 2022 | An Empirical Study on Data Distribution-Aware Test Selection for Deep Learning EnhancementabstractSimilar to traditional software that is constantly under evolution, deep neural networks need to evolve upon the rapid growth of test data for continuous enhancement (e.g., adapting to distribution shift in a new environment for deployment). However, it is labor intensive to manually label all of the collected test data. Test selection solves this problem by strategically choosing a small set to label. Via retraining with the selected set, deep neural networks will achieve competitive accuracy. Unfortunately, existing selection metrics involve three main limitations: (1) using different retraining processes, (2) ignoring data distribution shifts, and (3) being insufficiently evaluated. To fill this gap, we first conduct a systemically empirical study to reveal the impact of the retraining process and data distribution on model enhancement. Then based on our findings, we propose DAT, a novel distribution-aware test selection metric. Experimental results reveal that retraining using both the training and selected data outperforms using only the selected data. None of the selection metrics perform the best under various data distributions. By contrast, DAT effectively alleviates the impact of distribution shifts and outperforms the compared metrics by up to five times and 30.09% accuracy improvement for model enhancement on simulated and in-the-wild distribution shift scenarios, respectively. Yuejun Guo 0001, Maxime Cordy, Xiaofei Xie, Lei Ma 0003, Mike Papadakis, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 3 |
| 2021 | Towards Exploring the Limitations of Active Learning: An Empirical StudyabstractDeep neural networks (DNNs) are increasingly deployed as integral parts of software systems. However, due to the complex interconnections among hidden layers and massive hyperparameters, DNNs must be trained using a large number of labeled inputs, which calls for extensive human effort for collecting and labeling data. Spontaneously, to alleviate this growing demand, multiple state-of-the-art studies have developed different metrics to select a small yet informative dataset for the model training. These research works have demonstrated that DNN models can achieve competitive performance using a carefully selected small set of data. However, the literature lacks proper investigation of the limitations of data selection metrics, which is crucial to apply them in practice. In this paper, we fill this gap and conduct an extensive empirical study to explore the limits of data selection metrics. Our study involves 15 data selection metrics evaluated over 5 datasets (2 image classification tasks and 3 text classification tasks), 10 DNN architectures, and 20 labeling budgets (ratio of training data being labeled). Our findings reveal that, while data selection metrics are usually effective in producing accurate models, they may induce a loss of model robustness (against adversarial examples) and resilience to compression. Overall, we demonstrate the existence of a trade-off between labeling effort and different model qualities. This paves the way for future research in devising data selection metrics considering multiple quality criteria. Yuejun Guo 0001, Maxime Cordy, Xiaofei Xie, Wei Ma 0014, Mike Papadakis, Yves Le Traon |
ASE | 3 |
| 2021 | A Replication Study on the Usability of Code Vocabulary in Predicting Flaky TestsabstractIndustrial reports indicate that flaky tests are one of the primary concerns of software testing mainly due to the false signals they provide. To deal with this issue, researchers have developed tools and techniques aiming at (automatically) identifying flaky tests with encouraging results. However, to reach industrial adoption and practice, these techniques need to be replicated and evaluated extensively on multiple datasets, occasions and settings. In view of this, we perform a replication study of a recently proposed method that predicts flaky tests based on their vocabulary. We thus replicate the original study on three different dimensions. First, we replicate the approach on the same subjects as in the original study but using a different evaluation methodology, i.e., we adopt a time-sensitive selection of training and test sets to better reflect the envisioned use case. Second, we consolidate the findings of the initial study by building a new dataset of 837 flaky tests from 9 projects in a different programming language, i.e., Python while the original study was in Java, which comforts the generalisability of the results. Third, we propose an extension to the original approach by experimenting with different features extracted from the Code Under Test. We find that a more robust validation consistently decreases performance on the reported results of the original study, but, fortunately, the model remains capable to decently predict flaky tests. We find re-assuring results that the vocabulary-based models can also be used to predict test flakiness in Python. Finally, we find that the information lying in the Code Under Test has a limited impact on the performance of the vocabulary-based models. Guillaume Haben, Sarra Habchi, Mike Papadakis, Maxime Cordy, Yves Le Traon |
MSR | 4 |
| 2021 | Statistical model checking for variability-intensive systems: applications to bug detection and minimizationabstractAbstract We propose a new Statistical Model Checking (SMC) method to identify bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we propose to combine SMC with featured transition systems (FTS)—a model that represents jointly the state spaces of all variants. Our new methods allow the sampling of executions from one or more (potentially all) variants. We investigate their utility in two complementary use cases. The first case considers the problem of finding all variants that violate a given property expressed in Linear-Time Logic (LTL) within a given simulation budget. To achieve this, we perform random walks in the featured transition system seeking accepting lassos. We show that our method allows us to find bugs much faster (up to 16 times according to our experiments) than exhaustive methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a coarse-grained analysis method to quickly identify the set of buggy variants. The second case complements the first one. In case the coarse-grained analysis reveals that no variant can guarantee to satisfy an intended property in all their executions, one should identify the variant that minimizes the probability of violating this property. Thus, we propose a fine-grained SMC method that quickly identifies promising variants and accurately estimates their violation probability. We evaluate different selection strategies and reveal that a genetic algorithm combined with elitist selection yields the best results. Maxime Cordy, Sami Lazreg, Mike Papadakis, Axel Legay |
Formal Aspects Comput. | 1 |
| 2021 | A Formal Framework of Software Product Line AnalysesabstractA number of product-line analysis approaches lift analyses such as type checking, model checking, and theorem proving from the level of single programs to the level of product lines. These approaches share concepts and mechanisms that suggest an unexplored potential for reuse of key analysis steps and properties, implementation, and verification efforts. Despite the availability of taxonomies synthesizing such approaches, there still remains the underlying problem of not being able to describe product-line analyses and their properties precisely and uniformly. We propose a formal framework that models product-line analyses in a compositional manner, providing an overall understanding of the space of family-based, feature-based, and product-based analysis strategies. It defines precisely how the different types of product-line analyses compose and inter-relate. To ensure soundness, we formalize the framework, providing mechanized specification and proofs of key concepts and properties of the individual analyses. The formalization provides unambiguous definitions of domain terminology and assumptions as well as solid evidence of key properties based on rigorous formal proofs. To qualitatively assess the generality of the framework, we discuss to what extent it describes five representative product-line analyses targeting the following properties: safety, performance, dataflow facts, security, and functional program properties. Thiago M. Castro, Leopoldo Teixeira, Vander Alves, Sven Apel, Maxime Cordy, Rohit Gheyi |
ACM Trans. Softw. Eng. Methodol. | 5 |
| 2021 | Killing Stubborn Mutants with Symbolic ExecutionabstractWe introduce SEMu , a Dynamic Symbolic Execution technique that generates test inputs capable of killing stubborn mutants (killable mutants that remain undetected after a reasonable amount of testing). SEMu aims at mutant propagation (triggering erroneous states to the program output) by incrementally searching for divergent program behaviors between the original and the mutant versions. We model the mutant killing problem as a symbolic execution search within a specific area in the programs’ symbolic tree. In this framework, the search area is defined and controlled by parameters that allow scalable and cost-effective mutant killing. We integrate SEMu in KLEE and experimented with Coreutils (a benchmark frequently used in symbolic execution studies). Our results show that our modeling plays an important role in mutant killing. Perhaps more importantly, our results also show that, within a two-hour time limit, SEMu kills 37% of the stubborn mutants, where KLEE kills none and where the mutant infection strategy (strategy suggested by previous research) kills 17%. Thierry Titcheu Chekam, Mike Papadakis, Maxime Cordy, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 3 |
| 2021 | Test Selection for Deep Learning SystemsabstractTesting of deep learning models is challenging due to the excessive number and complexity of the computations involved. As a result, test data selection is performed manually and in an ad hoc way. This raises the question of how we can automatically select candidate data to test deep learning models. Recent research has focused on defining metrics to measure the thoroughness of a test suite and to rely on such metrics to guide the generation of new tests. However, the problem of selecting/prioritising test inputs (e.g., to be labelled manually by humans) remains open. In this article, we perform an in-depth empirical comparison of a set of test selection metrics based on the notion of model uncertainty (model confidence on specific inputs). Intuitively, the more uncertain we are about a candidate sample, the more likely it is that this sample triggers a misclassification. Similarly, we hypothesise that the samples for which we are the most uncertain are the most informative and should be used in priority to improve the model by retraining. We evaluate these metrics on five models and three widely used image classification problems involving real and artificial (adversarial) data produced by five generation algorithms. We show that uncertainty-based metrics have a strong ability to identify misclassified inputs, being three times stronger than surprise adequacy and outperforming coverage-related metrics. We also show that these metrics lead to faster improvement in classification accuracy during retraining: up to two times faster than random selection and other state-of-the-art metrics on all models we considered. Wei Ma 0014, Mike Papadakis, Anestis Tsakmalis, Maxime Cordy, Yves Le Traon |
ACM Trans. Softw. Eng. Methodol. | 4 |
| 2020 | Statistical Model Checking for Variability-Intensive SystemsabstractWe propose a new Statistical Model Checking (SMC) method to discover bugs in variability-intensive systems (VIS). The state-space of such systems is exponential in the number of variants, which makes the verification problem harder than for classical systems. To reduce verification time, we sample executions from a featured transition system – a model that represents jointly the state spaces of all variants. The combination of this compact representation and the inherent efficiency of SMC allows us to find bugs much faster (up to 16 times according to our experiments) than other methods. As any simulation-based approach, however, the risk of Type-1 error exists. We provide a lower bound and an upper bound for the number of simulations to perform to achieve the desired level of confidence. Our empirical study involving 59 properties over three case studies reveals that our method manages to discover all variants violating 41 of the properties. This indicates that SMC can act as a low-cost-high-reward method for verifying VIS. Maxime Cordy, Mike Papadakis, Axel Legay |
FASE | 1 |
| 2020 | Data-driven Simulation and Optimization for Covid-19 Exit StrategiesabstractThe rapid spread of the Coronavirus SARS-2 is a major challenge that led almost all governments worldwide to take drastic measures to respond to the tragedy. Chief among those measures is the massive lockdown of entire countries and cities, which beyond its global economic impact has created some deep social and psychological tensions within populations. While the adopted mitigation measures (including the lockdown) have generally proven useful, policymakers are now facing a critical question: how and when to lift the mitigation measures? A carefully-planned exit strategy is indeed necessary to recover from the pandemic without risking a new outbreak. Classically, exit strategies rely on mathematical modeling to predict the effect of public health interventions. Such models are unfortunately known to be sensitive to some key parameters, which are usually set based on rules-of-thumb. Salah Ghamizi, Renaud Rwemalika, Maxime Cordy, Lisa Veiber, Tegawendé F. Bissyandé, Mike Papadakis, Jacques Klein, Yves Le Traon |
KDD | 3 |
| 2020 | Search-based adversarial testing and improvement of constrained credit scoring systemsabstractCredit scoring systems are critical FinTech applications that concern the analysis of the creditworthiness of a person or organization. While decisions were previously based on human expertise, they are now increasingly relying on data analysis and machine learning. In this paper, we assess the ability of state-of-the-art adversarial machine learning to craft attacks on a real-world credit scoring system. Interestingly, we find that, while these techniques can generate large numbers of adversarial data, these are practically useless as they all violate domain-specific constraints. In other words, the generated examples are all false positives as they cannot occur in practice. To circumvent this limitation, we propose CoEvA2, a search-based method that generates valid adversarial examples (satisfying the domain constraints). CoEvA2 utilizes multi-objective search in order to simultaneously handle constraints, perform the attack and maximize the overdraft amount requested. We evaluate CoEvA2 on a major bank's real-world system by checking its ability to craft valid attacks. CoEvA2 generates thousands of valid adversarial examples, revealing a high risk for the banking system. Fortunately, by improving the system through adversarial training (based on the produced examples), we increase its robustness and make our attack fail. Salah Ghamizi, Maxime Cordy, Martin Gubri, Mike Papadakis, Andrey Boytsov, Yves Le Traon, Anne Goujon |
ESEC/SIGSOFT FSE | 2 |
| 2019 | Multifaceted automated analyses for variability-intensive embedded systemsabstractEmbedded systems, like those found in the automotive domain, must comply with stringent functional and non-functional requirements. To fulfil these requirements, engineers are confronted with a plethora of design alternatives both at the software and hardware level, out of which they must select the optimal solution wrt. possibly-antagonistic quality attributes (e.g. cost of manufacturing vs. speed of execution). We propose a model-driven framework to assist engineers in this choice. It captures high-level specifications of the system in the form of variable dataflows and configurable hardware platforms. A mapping algorithm then derives the design space, i.e. the set of compatible pairs of application and platform variants, and a variability-aware executable model, which encodes the functional and non-functional behaviour of all viable system variants. Novel verification algorithms then pinpoint the optimal system variants efficiently. The benefits of our approach are evaluated through a real-world case study from the automotive industry. Sami Lazreg, Maxime Cordy, Philippe Collet, Patrick Heymans, Sébastien Mosser 0001 |
ICSE | 2 |
| 2019 | Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet?abstractUniform or near-uniform generation of solutions for large satisfiability formulas is a problem of theoretical and practical interest for the testing community. Recent works proposed two algorithms (namely UniGen and QuickSampler) for reaching a good compromise between execution time and uniformity guarantees, with empirical evidence on SAT benchmarks. In the context of highly-configurable software systems (e.g., Linux), it is unclear whether UniGen and QuickSampler can scale and sample uniform software configurations. In this paper, we perform a thorough experiment on 128 real-world feature models. We find that UniGen is unable to produce SAT solutions out of such feature models. Furthermore, we show that QuickSampler does not generate uniform samples and that some features are either never part of the sample or too frequently present. Finally, using a case study, we characterize the impacts of these results on the ability to find bugs in a configurable system. Overall, our results suggest that we are not there: more research is needed to explore the cost-effectiveness of uniform sampling when testing large configurable systems. Quentin Plazar, Mathieu Acher, Gilles Perrouin, Xavier Devroey, Maxime Cordy |
ICST | 5 |
| 2019 | Search-based test and improvement of machine-learning-based anomaly detection systemsabstractMachine-learning-based anomaly detection systems can be vulnerable to new kinds of deceptions, known as training attacks, which exploit the live learning mechanism of these systems by progressively injecting small portions of abnormal data. The injected data seamlessly swift the learned states to a point where harmful data can pass unnoticed. We focus on the systematic testing of these attacks in the context of intrusion detection systems (IDS). We propose a search-based approach to test IDS by making training attacks. Going a step further, we also propose searching for countermeasures, learning from the successful attacks and thereby increasing the resilience of the tested IDS. We evaluate our approach on a denial-of-service attack detection scenario and a dataset recording the network traffic of a real-world system. Our experiments show that our search-based attack scheme generates successful attacks bypassing the current state-of-the-art defences. We also show that our approach is capable of generating attack patterns for all configuration states of the studied IDS and that it is capable of providing appropriate countermeasures. By co-evolving our attack and defence mechanisms we succeeded at improving the defence of the IDS under test by making it resilient to 49 out of 50 independently generated attacks. Maxime Cordy, Steve Muller, Mike Papadakis, Yves Le Traon |
ISSTA | 1 |
| 2019 | Verification and abstraction of real-time variability-intensive systems
Maxime Cordy, Axel Legay |
Int. J. Softw. Tools Technol. Transf. | 1 |
| 2018 | Are mutants really natural?: a study on how "naturalness" helps mutant selectionabstractBackground: Code is repetitive and predictable in a way that is similar to the natural language. This means that code is "natural" and this "naturalness" can be captured by natural language modelling techniques. Such models promise to capture the program semantics and identify source code parts that `smell', i.e., they are strange, badly written and are generally error-prone (likely to be defective). Aims: We investigate the use of natural language modelling techniques in mutation testing (a testing technique that uses artificial faults). We thus, seek to identify how well artificial faults simulate real ones and ultimately understand how natural the artificial faults can be. Our intuition is that natural mutants, i.e., mutants that are predictable (follow the implicit coding norms of developers), are semantically useful and generally valuable (to testers). We also expect that mutants located on unnatural code locations (which are generally linked with error-proneness) to be of higher value than those located on natural code locations. Method: Based on this idea, we propose mutant selection strategies that rank mutants according to a) their naturalness (naturalness of the mutated code), b) the naturalness of their locations (naturalness of the original program statements) and c) their impact on the naturalness of the code that they apply to (naturalness differences between original and mutated statements). We empirically evaluate these issues on a benchmark set of 5 open-source projects, involving more than 100k mutants and 230 real faults. Based on the fault set we estimate the utility (i.e. capability to reveal faults) of mutants selected on the basis of their naturalness, and compare it against the utility of randomly selected mutants. Results: Our analysis shows that there is no link between naturalness and the fault revelation utility of mutants. We also demonstrate that the naturalness-based mutant selection performs similar (slightly worse) to the random mutant selection. Conclusions: Our findings are negative but we consider them interesting as they confute a strong intuition, i.e., fault revelation is independent of the mutants' naturalness. Matthieu Jimenez, Thierry Titcheu Chekam, Maxime Cordy, Mike Papadakis, Marinos Kintis, Yves Le Traon, Mark Harman |
ESEM | 3 |
| 2018 | On the Impact of Tokenizer and Parameters on N-Gram Based Code AnalysisabstractRecent research shows that language models, such as n-gram models, are useful at a wide variety of software engineering tasks, e.g., code completion, bug identification, code summarisation, etc. However, such models require the appropriate set of numerous parameters. Moreover, the different ways one can read code essentially yield different models (based on the different sequences of tokens). In this paper, we focus on n-gram models and evaluate how the use of tokenizers, smoothing, unknown threshold and n values impact the predicting ability of these models. Thus, we compare the use of multiple tokenizers and sets of different parameters (smoothing, unknown threshold and n values) with the aim of identifying the most appropriate combinations. Our results show that the Modified Kneser-Ney smoothing technique performs best, while n values are depended on the choice of the tokenizer, with values 4 or 5 offering a good trade-off between entropy and computation time. Interestingly, we find that tokenizers treating the code as simple text are the most robust ones. Finally, we demonstrate that the differences between the tokenizers are of practical importance and have the potential of changing the conclusions of a given experiment. Matthieu Jimenez, Maxime Cordy, Yves Le Traon, Mike Papadakis |
ICSME | 2 |
| 2018 | TUNA: TUning Naturalness-Based AnalysisabstractNatural language processing techniques, in particular n-gram models, have been applied successfully to facilitate a number of software engineering tasks. However, in our related ICSME '18 paper, we have shown that the conclusions of a study can drastically change with respect to how the code is tokenized and how the used n-gram model is parameterized. These choices are thus of utmost importance, and one must carefully make them. To show this and allow the community to benefit from our work, we have developed TUNA (TUning Naturalness-based Analysis), a Java software artifact to perform naturalness-based analyses of source code. To the best of our knowledge, TUNA is the first open-source, end-to-end toolchain to carry out source code analyses based on naturalness. Matthieu Jimenez, Maxime Cordy, Yves Le Traon, Mike Papadakis |
ICSME | 2 |
| 2017 | Technical Aspect Extraction from Customer Reviews Based on Seeded Word Clustering
Jean-Marc Davril, Tony Leclercq, Maxime Cordy, Patrick Heymans |
NLDB | 3 |
| 2017 | On Featured Transition Systems
Axel Legay, Gilles Perrouin, Xavier Devroey, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans |
SOFSEM | 4 |
| 2017 | Statistical prioritization for software product line testing: an experience report
Xavier Devroey, Gilles Perrouin, Maxime Cordy, Hamza Samih, Axel Legay, Pierre-Yves Schobbens, Patrick Heymans |
Softw. Syst. Model. | 3 |
| 2015 | All-at-once-synthesis of controllers from scenario-based product line specificationsabstractSoftware-intensive systems often consist of multiple components that interact to realize complex requirements. An additional dimension of complexity arises when one designs many variants of a system at once, that is, a software product line (SPL). We propose a scenario-based approach to design SPLs, based on a combination of Modal Sequence Diagrams (MSDs) and a feature model. It consists in associating every MSD to the set of variants that have to satisfy its specification. Variability constitutes a new source of complexity, which can lead to inconsistencies in the specification of one or multiple variants. It is therefore crucial to detect these inconsistencies, and to produce a controller for each variant that makes it behave so that it satisfies its specification. We present a new controller synthesis technique that checks the absence of inconsistencies in all variants at once, thereby more radically exploiting the similarities between them. Our method first translates the MSD specification into a variability-aware Büchi game, and then solves this game for all variants in a single execution. We implemented the approach in ScenarioTools, a software tool which we use to evaluate our algorithms against competing methods. Maxime Cordy, Jean-Marc Davril, Joel Greenyer, Erika Gressi, Patrick Heymans |
SPLC | 1 |
| 2014 | Coverage Criteria for Behavioural Testing of Software Product Lines
Xavier Devroey, Gilles Perrouin, Axel Legay, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans |
ISoLA (1) | 4 |
| 2014 | Counterexample guided abstraction refinement of product-line behavioural modelsabstractThe model-checking problem for Software Products Lines (SPLs) is harder than for single systems: variability constitutes a new source of complexity that exacerbates the state-explosion problem. Abstraction techniques have successfully alleviated state explosion in single-system models. However, they need to be adapted to SPLs, to take into account the set of variants that produce a counterexample. In this paper, we apply CEGAR (Counterexample-Guided Abstraction Refinement) and we design new forms of abstraction specifically for SPLs. We carry out experiments to evaluate the efficiency of our new abstractions. The results show that our abstractions, combined with an appropriate refinement strategy, hold the potential to achieve large reductions in verification time, although they sometimes perform worse. We discuss in which cases a given abstraction should be used. Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens, Bruno Dawagne, Martin Leucker |
SIGSOFT FSE | 1 |
| 2014 | A variability perspective of mutation analysisabstractMutation testing is an effective technique for either improving or generating fault-finding test suites. It creates defective or incorrect program artifacts of the program under test and evaluates the ability of test suites to reveal them. Despite being effective, mutation is costly since it requires assessing the test cases with a large number of defective artifacts. Even worse, some of these artifacts are behaviourally ``equivalent'' to the original one and hence, they unnecessarily increase the testing effort. We adopt a variability perspective on mutation analysis. We model a defective artifact as a transition system with a specific feature selected and consider it as a member of a mutant family. The mutant family is encoded as a Featured Transition System, a compact formalism initially dedicated to model-checking of software product lines. We show how to evaluate a test suite against the set of all candidate defects by using mutant families. We can evaluate all the considered defects at the same time and isolate some equivalent mutants. We can also assist the test generation process and efficiently consider higher-order mutants. Xavier Devroey, Gilles Perrouin, Maxime Cordy, Mike Papadakis, Axel Legay, Pierre-Yves Schobbens |
SIGSOFT FSE | 3 |
| 2014 | Formal semantics, modular specification, and symbolic verification of product-line behaviour
Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens |
Sci. Comput. Program. | 2 |
| 2013 | Beyond boolean product-line model checking: dealing with feature attributes and multi-featuresabstractModel checking techniques for software product lines (SPL) are actively researched. A major limitation they currently have is the inability to deal efficiently with non-Boolean features and multi-features. An example of a non-Boolean feature is a numeric attribute such as maximum number of users which can take different numeric values across the range of SPL products. Multi-features are features that can appear several times in the same product, such as processing units which number is variable from one product to another and which can be configured independently. Both constructs are extensively used in practice but currently not supported by existing SPL model checking techniques. To overcome this limitation, we formally define a language that integrates these constructs with SPL behavioural specifications. We generalize SPL model checking algorithms correspondingly and evaluate their applicability. Our results show that the algorithms remain efficient despite the generalization. Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay |
ICSE | 1 |
| 2013 | Efficient quality assurance of variability-intensive systemsabstractVariability is becoming an increasingly important concern in software development but techniques to cost-effectively verify and validate software in the presence of variability have yet to become widespread. This half-day tutorial offers an overview of the state of the art in an emerging discipline at the crossroads of formal methods and software engineering: quality assurance of variability-intensive systems. We will present the most significant results obtained during the last four years or so, ranging from conceptual foundations to readily usable tools. Among the various quality assurance techniques, we focus on model checking, but also extend the discussion to other techniques. With its lightweight usage of mathematics and balance between theory and practice, this tutorial is designed to be accessible to a broad audience. Researchers working in the area, willing to join it, or simply curious, will get a comprehensive picture of the recent developments. Practitioners developing variability-intensive systems are invited to discover the capabilities of our techniques and tools, and to consider integrating them in their processes. Patrick Heymans, Axel Legay, Maxime Cordy |
ICSE | 3 |
| 2013 | Incrementally synthesizing controllers from scenario-based product line specificationsabstractMany software-intensive systems consist of components that interact to fulfill complex functionality. Moreover, often many variants of such systems have to be designed at once. This adds complexity to the design task. Recently, we proposed a scenario-based approach to design product lines, which combines feature diagrams and Modal Sequence Diagrams. We proposed a consistency-checking technique based on a dedicated product line model checker. One limitation of this technique is that it is incomplete, i.e., it may fail to show the consistency of some consistent specifications. In this paper we propose a new game-based approach that overcomes this incompleteness and, in addition, automatically synthesizes controllers for the consistent product specifications. We exploit the fact that many variants are similar and efficiently synthesize product controllers incrementally. We provide a prototype tool and evaluate the efficiency of the approach. Joel Greenyer, Christian Brenner 0001, Maxime Cordy, Patrick Heymans, Erika Gressi |
ESEC/SIGSOFT FSE | 3 |
| 2013 | Features meet scenarios: modeling and consistency-checking scenario-based product line specifications
Joel Greenyer, Amir Molzam Sharifloo, Maxime Cordy, Patrick Heymans |
Requir. Eng. | 3 |
| 2013 | Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model CheckingabstractThe premise of variability-intensive systems, specifically in software product line engineering, is the ability to produce a large family of different systems efficiently. Many such systems are critical. Thorough quality assurance techniques are thus required. Unfortunately, most quality assurance techniques were not designed with variability in mind. They work for single systems, and are too costly to apply to the whole system family. In this paper, we propose an efficient automata-based approach to linear time logic (LTL) model checking of variability-intensive systems. We build on earlier work in which we proposed featured transitions systems (FTSs), a compact mathematical model for representing the behaviors of a variability-intensive system. The FTS model checking algorithms verify all products of a family at once and pinpoint those that are faulty. This paper complements our earlier work, covering important theoretical aspects such as expressiveness and parallel composition as well as more practical things like vacuity detection and our logic feature LTL. Furthermore, we provide an in-depth treatment of the FTS model checking algorithm. Finally, we present SNIP, a new model checker for variability-intensive systems. The benchmarks conducted with SNIP confirm the speedups reported previously. Andreas Classen, Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, Jean-François Raskin |
IEEE Trans. Software Eng. | 2 |
| 2012 | Simulation-based abstractions for software product-line model checkingabstractSoftware Product Line (SPL) engineering is a software engineering paradigm that exploits the commonality between similar software products to reduce life cycle costs and time-to-market. Many SPLs are critical and would benefit from efficient verification through model checking. Model checking SPLs is more difficult than for single systems, since the number of different products is potentially huge. In previous work, we introduced Featured Transition Systems (FTS), a formal, compact representation of SPL behaviour, and provided efficient algorithms to verify FTS. Yet, we still face the state explosion problem, like any model checking-based verification. Model abstraction is the most relevant answer to state explosion. In this paper, we define a novel simulation relation for FTS and provide an algorithm to compute it. We extend well-known simulation preservation properties to FTS and thus lay the theoretical foundations for abstraction-based model checking of SPLs. We evaluate our approach by comparing the cost of FTS-based simulation and abstraction with respect to product-by-product methods. Our results show that FTS are a solid foundation for simulation-based model checking of SPL. Maxime Cordy, Andreas Classen, Gilles Perrouin, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay |
ICSE | 1 |
| 2012 | A Vision for Behavioural Model-Driven Validation of Software Product Lines
Xavier Devroey, Maxime Cordy, Gilles Perrouin, Eun-Young Kang 0001, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay, Benoit Baudry |
ISoLA (1) | 2 |
| 2012 | Efficient consistency checking of scenario-based product-line specificationsabstractModern technical systems typically consist of multiple components and must provide many functions that are realized by the complex interaction of these components. Moreover, very often not only a single product, but a whole product line with different compositions of components and functions must be developed. To cope with this complexity, it is important that engineers have intuitive, but precise means for specifying the requirements for these systems and have tools for automatically finding inconsistencies within the requirements, because these could lead to costly iterations in the later development. We propose a technique for the scenario-based specification of component interactions based on Modal Sequence Diagrams. Moreover, we developed an efficient technique for automatically finding inconsistencies in the scenario-based specification of many variants at once by exploiting recent advances in the model-checking of product lines. Our evaluation shows benefits of this technique over performing individual consistency checking of each variant specification. Joel Greenyer, Amir Molzam Sharifloo, Maxime Cordy, Patrick Heymans |
RE | 3 |
| 2012 | Behavioural modelling and verification of real-time software product linesabstractIn Software Product Line (SPL) engineering, software products are build in families rather than individually. Many critical software are nowadays build as SPLs and most of them obey hard real-time requirements. Formal methods for verifying SPLs are thus crucial and actively studied. The verification problem for SPL is, however, more complicated than for individual systems; the large number of different software products multiplies the complexity of SPL model-checking. Recently, promising model-checking approaches have been developed specifically for SPLs. They leverage the commonality between the products to reduce the verification effort. However, none of them considers real time. Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay |
SPLC (1) | 1 |
| 2012 | Towards an incremental automata-based approach for software product-line model checkingabstractMost model-checking algorithms are based on automata theory. For instance, determining whether or not a transition system satisfies a Linear Temporal Logic (LTL) formula requires computing strongly connected component of its transition graph. In Software Product-Line (SPL) engineering, the model checking problem is more complex due to the huge amount of software products that may compose the line. Indeed, one has to determine the exact subset of those products that do not satisfy an intended property. Efficient dedicated verification methods have been recently developed to answer this problem. However, most of them does not allow incremental verification. In this paper, we introduce an automata-based incremental approach for SPL model checking. Our method makes use of previous results to determine whether or not the addition of conservative features (i.e., features that do not remove behaviour from the system) preserves the satisfaction of properties expressed in LTL. We provide a detailed description of the approach and propose algorithms that implement it. We discuss how our method can be combined with SPL dedicated verification methods, viz. Featured Transition Systems. Maxime Cordy, Pierre-Yves Schobbens, Patrick Heymans, Axel Legay |
SPLC (2) | 1 |
| 2012 | Model checking software product lines with SNIP
Andreas Classen, Maxime Cordy, Patrick Heymans, Axel Legay, Pierre-Yves Schobbens |
Int. J. Softw. Tools Technol. Transf. | 2 |