Sufficient Preconditions for Modular Assertion Checking. - Yannick Moy (VMCAI, 2008)

Modular inference of subprogram contracts for safety checking. - Yannick Moy; Claude Marché (J. Symb. Comput., 2010)

Correct Code Containing Containers. - Claire Dross; Jean-Christophe Filliâtre; Yannick Moy (TAP@TOOLS, 2011)

Hi-Lite - Verification by Contract. - Johannes Kanig; Jérôme Guitton; Yannick Moy (Softwaretechnik-Trends, 2011)

Source Code as the Key Artifact in Requirement-Based Development: The Case of Ada 2012. - José F. Ruiz; Cyrille Comar; Yannick Moy (Ada-Europe, 2012)

Integration von Formaler Verifikation und Test. - Cyrille Comar; Johannes Kanig; Yannick Moy (Automotive - Safety & Security, 2012)

Maximal and Compositional Pattern-Based Loop Invariants. - Maria-Virginia Aponte; Pierre Courtieu; Yannick Moy; Marc Sango (FM, 2012)

Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. - Yannick Moy; Emmanuel Ledinot; Hervé Delseny; Virginie Wiels; Benjamin Monate (IEEE Softw., 2013)

Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification. - Johannes Kanig; Roderick Chapman; Cyrille Comar; Jérôme Guitton; Yannick Moy; Emyr Rees (TAP@STAF, 2014)

SPARK 2014 and GNATprove - A competition report from builders of an industrial-strength verifying compiler. - Duc Hoang; Yannick Moy; Angela Wallenburg; Roderick Chapman (Int. J. Softw. Tools Technol. Transf., 2015)

High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles. - S. Tucker Taft; Florian Schanda; Yannick Moy (HASE, 2016)

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. - Nikolai Kosmatov; Claude Marché; Yannick Moy; Julien Signoles (ISoLA (1), 2016)

Abstract Software Specifications and Automatic Proof of Refinement. - Claire Dross; Yannick Moy (RSSRail, 2016)

Counterexamples from Proof Failures in SPARK. - David Hauzar; Claude Marché; Yannick Moy (SEFM, 2016)

Auto-Active Proof of Red-Black Trees in SPARK. - Claire Dross; Yannick Moy (NFM, 2017)

Focused Certification of an Industrial Compilation and Static Verification Toolchain. - Zhi Zhang; Robby; John Hatcliff; Yannick Moy; Pierre Courtieu (SEFM, 2017)

Automating the Verification of Floating-Point Programs. - Clément Fumex; Claude Marché; Yannick Moy (VSTTE, 2017)

Safe Dynamic Memory Management in Ada and SPARK. - Maroua Maalej; S. Tucker Taft; Yannick Moy (Ada-Europe, 2018)

Borrowing Safe Pointers from Rust in SPARK. - Georges-Axel Jaloyan; Yannick Moy; Andrei Paskevich (CoRR, 2018)

Lightweight Interactive Proving inside an Automatic Program Verifier. - Sylvain Dailler; Claude Marché; Yannick Moy (F-IDE@FLoC, 2018)

Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software. - Yannick Moy (Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018)

Instrumenting a weakest precondition calculus for counterexample generation. - Sylvain Dailler; David Hauzar; Claude Marché; Yannick Moy (J. Log. Algebraic Methods Program., 2018)

Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK. - Benjamin M. Brosgol; Claire Dross; Yannick Moy (SecDev, 2019)

Verification of Programs with Pointers in SPARK. - Georges-Axel Jaloyan; Claire Dross; Maroua Maalej; Yannick Moy; Andrei Paskevich (ICFEM, 2020)

Layered Formal Verification of a TCP Stack. - Guillaume Cluzel; Kyriakos Georgiou; Yannick Moy; Clément Zeller (SecDev, 2021)

How the Analyzer can Help the User Help the Analyzer. - Yannick Moy (F-IDE@NFM, 2021)

Security-Hardening Software Libraries with Ada and SPARK - A TCP Stack Use Case. - Kyriakos Georgiou; Guillaume Cluzel; Paul Butcher; Yannick Moy (CoRR, 2021)

Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library. - Aïssata Maiga; Cyrille Artho; Florian Gilcher; Yannick Moy (FTSCS, 2023)

Co-Developing Programs and Their Proof of Correctness. - Roderick Chapman; Claire Dross; Stuart Matthews; Yannick Moy (Commun. ACM, 2024)