1 citations · 1 across the 2 of their papers we have counts for
4 papers
Security-Hardening Software Libraries with Ada and SPARK -- A TCP Stack Use Case
Kyriakos Georgiou, Guillaume Cluzel, Paul Butcher +1
This white paper demonstrates how the assurance, reliability, and security of an existing professional-grade, open-source embedded TCP/IP stack implementation written in the C prog…
How the Analyzer can Help the User Help the Analyzer
Yannick Moy
The automation offered by modern program proof tools goes hand in hand with the capability to interact with the tool when the verification fails. The SPARK proof tool tries to help…
Lightweight Interactive Proving inside an Automatic Program Verifier
Sylvain Dailler, Claude Marché, Yannick Moy
Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of hu…
Borrowing Safe Pointers from Rust in SPARK
Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich
In the field of deductive software verification, programs with pointers present a major challenge due to pointer aliasing. In this paper, we introduce pointers to SPARK, a well-def…