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…