34 citations · 41 across the 11 of their papers we have counts for
12 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…
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…
Proceedings 4th Workshop on Formal Integrated Development Environment
Paolo Masci, Rosemary Monahan, Virgile Prevosto
This volume contains the proceedings of F-IDE 2018, the fourth international workshop on Formal Integrated Development Environment, which was held as a FLoC 2018 satellite event, o…
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…
Left-eigenvectors are certificates of the Orbit Problem
Steven de Oliveira, Virgile Prevosto, Peter Habermehl +1
This paper investigates the connexion between the Kannan-Lipton Orbit Problem and the polynomial invariant generator algorithm PILA based on eigenvectors computation. Namely, we re…
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…
Synthesizing invariants by solving solvable loops
Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
When proving invariance properties of a program, we face two problems. The first problem is related to the necessity of proving tautologies of considered assertion language, wherea…
Polynomial invariants by linear algebra
Steven de Oliveira, Saddek Bensalem, Virgile Prevosto
We present in this paper a new technique for generating polynomial invariants, divided in two independent parts : a procedure that reduces polynomial assignments composed loops ana…
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…