5 citations · 5 across the 4 of their papers we have counts for
4 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…
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…
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…