16 citations
Counting papers with at most 25 authors, so collaboration author lists do not stand in for the people here.
- Université Paris-SaclayFR3 papers
- Université Paris-SudFR2 papers
- Board of the Swiss Federal Institutes of TechnologyCH1 paper
- Centre Inria de SaclayFR1 paper
- Centre National de la Recherche ScientifiqueFR1 paper
- ETH ZurichCH1 paper
- Laboratoire de Recherche en InformatiqueFR1 paper
- National University of Ireland, MaynoothIE1 paper
- The University of MelbourneAU1 paper
- TOCCATA: Certified Programs, Certified Tools, Certified Floating-Point ComputationsFR1 paper
- Università della Svizzera italianaCH1 paper
- Université Paris Sciences et LettresFR1 paper
4 papers
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…
VerifyThis 2019: A Program Verification Competition (Extended Report)
Claire Dross, Carlo A. Furia, Marieke Huisman +2
VerifyThis is a series of program verification competitions that emphasize the human aspect: participants tackle the verification of detailed behavioral properties -- something tha…
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…