34 citations · 45 across the 15 of their papers we have counts for
15 papers
An Efficient VCGen-based Modular Verification of Relational Properties
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto +1
Deductive verification typically relies on function contracts that specify the behavior of each function for a single function call. Relational properties link several function cal…
Execution at RISC: Stealth JOP Attacks on RISC-V Applications
Loïc Buckwell, Olivier Gilles, Daniel Gracia Pérez +1
RISC-V is a recently developed open instruction set architecture gaining a lot of attention. To achieve a lasting security on these systems and design efficient countermeasures, a…
Towards Formal Verification of a TPM Software Stack
Yani Ziani, Nikolai Kosmatov, Frédéric Loulergue +2
The Trusted Platform Module (TPM) is a cryptoprocessor designed to protect integrity and security of modern computers. Communications with the TPM go through the TPM Software Stack…
An Efficient Black-Box Support of Advanced Coverage Criteria for Klee
Nicolas Berthier, Steven De Oliveira, Nikolai Kosmatov +2
Dynamic symbolic execution (DSE) is a powerful test generation approach based on an exploration of the path space of the program under test. Well-adapted for path coverage, this ap…
Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming
Olivier Gilles, Franck Viguier, Nikolai Kosmatov +1
RISC-V is an open instruction set architecture recently developed for embedded real-time systems. To achieve a lasting security on these systems and design efficient countermeasure…
Certified Verification of Relational Properties
Lionel Blatter, Nikolai Kosmatov, Virgile Prevosto +1
The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls t…
Abstract Compilation for Verification of Numerical Accuracy Properties
Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov +2
Verification of numerical accuracy properties in modern software remains an important and challenging task. This paper describes an original framework combining different solutions…
MetAcsl: Specification and Verification of High-Level Properties
Virgile Robles, Nikolai Kosmatov, Virgile Prevosto +2
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global v…
Static and Dynamic Verification of Relational Properties on Self-Composed C Code
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall +2
Function contracts are a well-established way of formally specifying the intended behavior of a function. However, they usually only describe what should happen during a single cal…
Freeing Testers from Polluting Test Objectives
Michaël Marcozzi, Sébastien Bardin, Nikolai Kosmatov +3
Testing is the primary approach for detecting software defects. A major challenge faced by testers lies in crafting efficient test suites, able to detect a maximum number of bugs w…
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic a…
Generic and Effective Specification of Structural Test Objectives
Sébastien Bardin, Mickaël Delahaye, Nikolai Kosmatov +2
While a wide range of different, sometimes heterogeneous test coverage criteria have been proposed, there exists no generic formalism to describe them, and available test automatio…
RPP: Automatic Proof of Relational Properties by Self-Composition
Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall +1
Self-composition provides a powerful theoretical approach to prove relational properties, i.e. properties relating several program executions, that has been applied to compare two…
Your Proof Fails? Testing Helps to Find the Reason
Guillaume Petiot, Nikolai Kosmatov, Bernard Botella +2
Applying deductive verification to formally prove that a program respects its formal specification is a very complex and time-consuming task due in particular to the lack of feedba…
Efficient Leverage of Symbolic ATG Tools to Advanced Coverage Criteria
Sébastien Bardin, Nikolai Kosmatov, François Cheynier
Automatic test data generation (ATG) is a major topic in software engineering. In this paper, we seek to bridge the gap between the coverage criteria supported by symbolic ATG tool…