34 citations · 41 across the 11 of their papers we have counts for
8 papers · 1 filter
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…
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…
Proceedings Fifth Workshop on Formal Integrated Development Environment
Rosemary Monahan, Virgile Prevosto, Jose Proença
This volume contains the proceedings of F-IDE 2019, the fifth international workshop on Formal Integrated Development Environment, which was held on October 7, 2019 in Porto, Portu…
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…
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…