Yannick Moy

Publication Activity (10 Years)

Years Active: 2008-2024
Publications (10 Years): 20

Top Topics

Formal Verification

Top Venues

Publications

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