Yannick Moy

29 papers B 4C 1Misc 2Journal 9Unranked 13
YearRankTypeTitle / Venue / Authors
2024 J jnl
Co-Developing Programs and Their Proof of Correctness.
Commun. ACM
Roderick Chapman, Claire Dross, Stuart Matthews, Yannick Moy
2023 — conf
Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library.
FTSCS
Aïssata Maiga, Cyrille Artho, Florian Gilcher, Yannick Moy
2021 — conf
How the Analyzer can Help the User Help the Analyzer.
F-IDE@NFM
Yannick Moy
2021 — conf
Layered Formal Verification of a TCP Stack.
SecDev
Guillaume Cluzel, Kyriakos Georgiou, Yannick Moy, Clément Zeller
2021 J jnl
Security-Hardening Software Libraries with Ada and SPARK - A TCP Stack Use Case.
CoRR
Kyriakos Georgiou, Guillaume Cluzel, Paul Butcher, Yannick Moy
2020 C conf
Verification of Programs with Pointers in SPARK.
ICFEM
Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich
2019 — conf
Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK.
SecDev
Benjamin M. Brosgol, Claire Dross, Yannick Moy
2018 J jnl
Borrowing Safe Pointers from Rust in SPARK.
CoRR
Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich
2018 J jnl
Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software.
Electron. Commun. Eur. Assoc. Softw. Sci. Technol.
Yannick Moy
2018 J jnl
Instrumenting a weakest precondition calculus for counterexample generation.
J. Log. Algebraic Methods Program.
Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy
2018 — conf
Lightweight Interactive Proving inside an Automatic Program Verifier.
F-IDE@FLoC
Sylvain Dailler, Claude Marché, Yannick Moy
2018 Misc conf
Safe Dynamic Memory Management in Ada and SPARK.
Ada-Europe
Maroua Maalej, S. Tucker Taft, Yannick Moy
2017 — conf
Auto-Active Proof of Red-Black Trees in SPARK.
NFM
Claire Dross, Yannick Moy
2017 — conf
Automating the Verification of Floating-Point Programs.
VSTTE
Clément Fumex, Claude Marché, Yannick Moy
2017 B conf
Focused Certification of an Industrial Compilation and Static Verification Toolchain.
SEFM
Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu
2016 — conf
Abstract Software Specifications and Automatic Proof of Refinement.
RSSRail
Claire Dross, Yannick Moy
2016 B conf
Counterexamples from Proof Failures in SPARK.
SEFM
David Hauzar, Claude Marché, Yannick Moy
2016 — conf
High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles.
HASE
S. Tucker Taft, Florian Schanda, Yannick Moy
2016 — conf
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.
ISoLA (1)
Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
2015 J jnl
SPARK 2014 and GNATprove - A competition report from builders of an industrial-strength verifying compiler.
Int. J. Softw. Tools Technol. Transf.
Duc Hoang, Yannick Moy, Angela Wallenburg, Roderick Chapman
2014 — conf
Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification.
TAP@STAF
Johannes Kanig, Roderick Chapman, Cyrille Comar, Jérôme Guitton, Yannick Moy, Emyr Rees
2013 J jnl
Testing or Formal Verification: DO-178C Alternatives and Industrial Experience.
IEEE Softw.
Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, Benjamin Monate
2012 — conf
Integration von Formaler Verifikation und Test.
Automotive - Safety & Security
Cyrille Comar, Johannes Kanig, Yannick Moy
2012 B conf
Maximal and Compositional Pattern-Based Loop Invariants.
FM
Maria-Virginia Aponte, Pierre Courtieu, Yannick Moy, Marc Sango
2012 Misc conf
Source Code as the Key Artifact in Requirement-Based Development: The Case of Ada 2012.
Ada-Europe
José F. Ruiz, Cyrille Comar, Yannick Moy
2011 — conf
Correct Code Containing Containers.
TAP@TOOLS
Claire Dross, Jean-Christophe Filliâtre, Yannick Moy
2011 J jnl
Hi-Lite - Verification by Contract.
Softwaretechnik-Trends
Johannes Kanig, Jérôme Guitton, Yannick Moy
2010 J jnl
Modular inference of subprogram contracts for safety checking.
J. Symb. Comput.
Yannick Moy, Claude Marché
2008 B conf
Sufficient Preconditions for Modular Assertion Checking.
VMCAI
Yannick Moy