1 citations · 1 across the 4 of their papers we have counts for
5 papers
Control-Flow Integrity at RISC: Attacking RISC-V by Jump-Oriented Programming
Olivier Gilles, Franck Viguier, Nikolai Kosmatov +1
RISC-V is an open instruction set architecture recently developed for embedded real-time systems. To achieve a lasting security on these systems and design efficient countermeasure…
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…
Abstract Compilation for Verification of Numerical Accuracy Properties
Maxime Jacquemin, Fonenantsoa Maurica, Nikolai Kosmatov +2
Verification of numerical accuracy properties in modern software remains an important and challenging task. This paper describes an original framework combining different solutions…
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…
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Allan Blanchard, Frédéric Loulergue, Nikolai Kosmatov
Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic a…