Add few Ltest publications

_data/publications.yml

@@ -20,6 +20,8 @@
   plugins:
   - id: cfp
     name: CFP
+  - id: ltest
+    name: LTest
   - id: metacsl
     name: MetACSL
   - id: pathcrawler

_fc-publications/ltest/2014-tap-bcdk.md

+---
+plugin: "ltest"
+authors: "Sébastien Bardin, Omar Chebaro, Mickaël Delahaye, and Nikolai Kosmatov"
+title: "An All-in-One Toolkit for Automated White-Box Testing"
+book: "International Conference on Tests and Proofs (TAP)"
+link: https://hal-cea.archives-ouvertes.fr/cea-01834983v1
+year: 2014
+category: foundational
+---
+
+Automated white-box testing is a major issue in software engineering. Over the years, several tools have been proposed for supporting distinct parts of the testing process. Yet, these tools are mostly separated and most of them support only a fixed and restricted subset of testing criteria. We describe in this paper Frama-C/LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest provides a unified support of many different testing criteria as well as an easy integration of new criteria. Moreover, it is designed around three basic services (test coverage estimation, automatic test generation, detection of uncoverable objectives) covering most major aspects of white-box testing and taking benefit from a combination of static and dynamic analyses. Services can cooperate through a shared coverage database. Preliminary experiments demonstrate the possibilities and advantages of such cooperations.
\ No newline at end of file

_fc-publications/ltest/2017-icst-mbdkv.md

+---
+plugin: "ltest"
+authors: "Michaël Marcozzi, Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov, and Virgile Prevosto"
+title: "Taming Coverage Criteria Heterogeneity with LTest"
+book: "International Conference on Software Testing, Verification and Validation (ICST)"
+link: https://hal-cea.archives-ouvertes.fr/cea-01808788v1
+year: 2017
+category: foundational
+---
+
+Automated white-box testing is a major issue in software engineering. In previous work, we introduced LTest, a generic and integrated toolkit for automated white-box testing of C programs. LTest supports a broad class of coverage criteria in a unified way (through the label specification mechanism) and covers most major parts of the testing process - including coverage measurement, test generation and detection of infeasible test objectives. However, the original version of LTest was unable to handle several major classes of coverage criteria, such as MCDC or dataflow criteria. Moreover, its practical applicability remained barely assessed. In this work, we present a significantly extended version of LTest that supports almost all existing testing criteria, including MCDC and some software security properties, through a native support of recently proposed hyperlabels. We also provide a more realistic view on the practical applicability of the extended tool, with experiments assessing its efficiency and scalability on real-world programs.
\ No newline at end of file

_fc-publications/ltest/2018-icse-mpbkpc.md

+---
+plugin: "ltest"
+authors: "Michaël Marcozzi, Mike Papadakis, Sébastien Bardin, Nikolai Kosmatov, Virgile Prévosto, and Loic Correnson"
+title: "Time to Clean Your Test Objectives"
+book: "International Conference On Software Engineering (ICSE)"
+link: https://hal-cea.archives-ouvertes.fr/cea-01835503
+year: 2018
+category: foundational
+---
+
+Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting eecient test suites, able to detect a maximum number of bugs with manageable eeort. To do so, they rely on coverage criteria, which deene some precise test objectives to be covered. However, many common criteria specify a signiicant number of objectives that occur to be infeasible or redundant in practice, like covering dead code or semantically equal mutants. Such objectives are well-known to be harmful to the design of test suites, impacting both the eeciency and precision of the tester's eeort. This work introduces a sound and scalable technique to prune out a signiicant part of the infeasible and redundant objectives produced by a panel of white-box criteria. In a nutshell, we reduce this task to proving the validity of logical assertions in the code under test. The technique is implemented in a tool that relies on weakest-precondition calculus and SMT solving for proving the assertions. The tool is built on top of the Frama-C veriication platform, which we carefully tune for our speciic scalability needs. The experiments reveal that the pruning capabilities of the tool can reduce the number of targeted test objectives in a program by up to 27% and scale to real programs of 200K lines, making it possible to automate a painstaking part of their current testing process.
\ No newline at end of file

_fc-publications/ltest/2020-ifm-mkpl.md

+---
+plugin: "ltest"
+authors: "Thibault Martin, Nikolai Kosmatov, Virgile Prevosto, and Matthieu Lemerre"
+title: "Detection of Polluting Test Objectives for Dataflow Criteria"
+book: "International Conference on Integrated Formal Methods (IFM)"
+link: https://hal-cea.archives-ouvertes.fr/cea-02974228
+year: 2020
+category: foundational
+---
+
+Dataflow test coverage criteria, such as all-defs and all-uses, belong to the most advanced coverage criteria. These criteria are defined by complex artifacts combining variable definitions, uses and program paths. Detection of polluting (i.e. inapplicable, infeasible and equivalent) test objectives for such criteria is a particularly challenging task. This short paper evaluates three detection approaches involving dataflow analysis, value analysis and weakest precondition calculus. We implement and compare these approaches, analyze their detection capacities and propose a methodology for their efficient combination. Initial experiments illustrate the benefits of the proposed approach.
\ No newline at end of file