Yannick Moy

According to our database, Yannick Moy authored at least 29 papers between 2008 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

Co-Developing Programs and Their Proof of Correctness.

Roderick Chapman, Claire Dross, Stuart Matthews, Yannick Moy

Commun. ACM, March, 2024

2023

Does Rust SPARK Joy? Safe Bindings from Rust to SPARK, Applied to the BBQueue Library.

Aïssata Maiga, Cyrille Artho, Florian Gilcher, Yannick Moy

Proceedings of the 9th ACM SIGPLAN International Workshop on Formal Techniques for Safety-Critical Systems, 2023

2021

Security-Hardening Software Libraries with Ada and SPARK - A TCP Stack Use Case.

Kyriakos Georgiou, Guillaume Cluzel, Paul Butcher, Yannick Moy

CoRR, 2021

How the Analyzer can Help the User Help the Analyzer.

Yannick Moy

Proceedings of the 6th Workshop on Formal Integrated Development Environment, 2021

Layered Formal Verification of a TCP Stack.

Guillaume Cluzel, Kyriakos Georgiou, Yannick Moy, Clément Zeller

Proceedings of the IEEE Secure Development Conference, 2021

2020

Verification of Programs with Pointers in SPARK.

Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich

Proceedings of the Formal Methods and Software Engineering, 2020

2019

Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK.

Benjamin M. Brosgol, Claire Dross, Yannick Moy

Proceedings of the 2019 IEEE Cybersecurity Development, 2019

2018

Instrumenting a weakest precondition calculus for counterexample generation.

Sylvain Dailler, David Hauzar, Claude Marché, Yannick Moy

J. Log. Algebraic Methods Program., 2018

Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software.

Yannick Moy

Electron. Commun. Eur. Assoc. Softw. Sci. Technol., 2018

Lightweight Interactive Proving inside an Automatic Program Verifier.

Sylvain Dailler, Claude Marché, Yannick Moy

Proceedings of the Proceedings 4th Workshop on Formal Integrated Development Environment, 2018

Borrowing Safe Pointers from Rust in SPARK.

Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich

CoRR, 2018

Safe Dynamic Memory Management in Ada and SPARK.

Maroua Maalej, S. Tucker Taft, Yannick Moy

Proceedings of the Reliable Software Technologies - Ada-Europe 2018, 2018

2017

Automating the Verification of Floating-Point Programs.

Clément Fumex, Claude Marché, Yannick Moy

Proceedings of the Verified Software. Theories, Tools, and Experiments, 2017

Focused Certification of an Industrial Compilation and Static Verification Toolchain.

Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu

Proceedings of the Software Engineering and Formal Methods - 15th International Conference, 2017

Auto-Active Proof of Red-Black Trees in SPARK.

Claire Dross, Yannick Moy

Proceedings of the NASA Formal Methods - 9th International Symposium, 2017

2016

Counterexamples from Proof Failures in SPARK.

David Hauzar, Claude Marché, Yannick Moy

Proceedings of the Software Engineering and Formal Methods - 14th International Conference, 2016

Abstract Software Specifications and Automatic Proof of Refinement.

Claire Dross, Yannick Moy

Proceedings of the Reliability, Safety, and Security of Railway Systems. Modelling, Analysis, Verification, and Certification, 2016

Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014.

Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles

Proceedings of the Leveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques, 2016

High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles.

S. Tucker Taft, Florian Schanda, Yannick Moy

Proceedings of the 17th IEEE International Symposium on High Assurance Systems Engineering, 2016

2015

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

2014

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

Proceedings of the Tests and Proofs - 8th International Conference, 2014

2013

Testing or Formal Verification: DO-178C Alternatives and Industrial Experience.

Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, Benjamin Monate

IEEE Softw., 2013

2012

Maximal and Compositional Pattern-Based Loop Invariants.

Maria-Virginia Aponte, Pierre Courtieu, Yannick Moy, Marc Sango

Proceedings of the FM 2012: Formal Methods, 2012

Integration von Formaler Verifikation und Test.

Cyrille Comar, Johannes Kanig, Yannick Moy

Proceedings of the Automotive, 2012

Source Code as the Key Artifact in Requirement-Based Development: The Case of Ada 2012.

José F. Ruiz, Cyrille Comar, Yannick Moy

Proceedings of the Reliable Software Technologies - Ada-Europe 2012, 2012

2011

Hi-Lite - Verification by Contract.

Johannes Kanig, Jérôme Guitton, Yannick Moy

Softwaretechnik-Trends, 2011

Correct Code Containing Containers.

Claire Dross, Jean-Christophe Filliâtre, Yannick Moy

Proceedings of the Tests and Proofs - 5th International Conference, 2011

2010

Modular inference of subprogram contracts for safety checking.

Yannick Moy, Claude Marché

J. Symb. Comput., 2010

2008

Sufficient Preconditions for Modular Assertion Checking.

Yannick Moy

Proceedings of the Verification, 2008