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…