default search action
Yannick Moy
Person information
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
2020 – today
- 2024
- [j7]Roderick Chapman, Claire Dross, Stuart Matthews
, Yannick Moy:
Co-Developing Programs and Their Proof of Correctness. Commun. ACM 67(3): 84-94 (2024) - 2023
- [c20]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: 37-47 - 2021
- [c19]Guillaume Cluzel, Kyriakos Georgiou, Yannick Moy, Clément Zeller:
Layered Formal Verification of a TCP Stack. SecDev 2021: 86-93 - [c18]Yannick Moy:
How the Analyzer can Help the User Help the Analyzer. F-IDE@NFM 2021: 97-104 - [i2]Kyriakos Georgiou, Guillaume Cluzel, Paul Butcher, Yannick Moy:
Security-Hardening Software Libraries with Ada and SPARK - A TCP Stack Use Case. CoRR abs/2109.10347 (2021) - 2020
- [c17]Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy, Andrei Paskevich:
Verification of Programs with Pointers in SPARK. ICFEM 2020: 55-72
2010 – 2019
- 2019
- [c16]Benjamin M. Brosgol, Claire Dross, Yannick Moy:
Tutorial: A Practical Introduction to Formal Development and Verification of High-Assurance Software with SPARK. SecDev 2019: 1-2 - 2018
- [j6]Yannick Moy:
Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software. Electron. Commun. Eur. Assoc. Softw. Sci. Technol. 76 (2018) - [j5]Sylvain Dailler, David Hauzar
Instrumenting a weakest precondition calculus for counterexample generation. J. Log. Algebraic Methods Program. 99: 97-113 (2018) - [c15]Maroua Maalej, S. Tucker Taft, Yannick Moy:
Safe Dynamic Memory Management in Ada and SPARK. Ada-Europe 2018: 37-52 - [c14]Sylvain Dailler, Claude Marché, Yannick Moy:
Lightweight Interactive Proving inside an Automatic Program Verifier. F-IDE@FLoC 2018: 1-15 - [i1]Georges-Axel Jaloyan, Yannick Moy, Andrei Paskevich:
Borrowing Safe Pointers from Rust in SPARK. CoRR abs/1805.05576 (2018) - 2017
- [c13]Claire Dross, Yannick Moy:
Auto-Active Proof of Red-Black Trees in SPARK. NFM 2017: 68-83 - [c12]Zhi Zhang, Robby, John Hatcliff, Yannick Moy, Pierre Courtieu:
Focused Certification of an Industrial Compilation and Static Verification Toolchain. SEFM 2017: 17-34 - [c11]Clément Fumex, Claude Marché, Yannick Moy:
Automating the Verification of Floating-Point Programs. VSTTE 2017: 102-119 - 2016
- [c10]S. Tucker Taft, Florian Schanda, Yannick Moy:
High-Integrity Multitasking in SPARK: Static Detection of Data Races and Locking Cycles. HASE 2016: 238-239 - [c9]Nikolai Kosmatov, Claude Marché, Yannick Moy, Julien Signoles
Static versus Dynamic Verification in Why3, Frama-C and SPARK 2014. ISoLA (1) 2016: 461-478 - [c8]Claire Dross, Yannick Moy:
Abstract Software Specifications and Automatic Proof of Refinement. RSSRail 2016: 215-230 - [c7]David Hauzar, Claude Marché, Yannick Moy:
Counterexamples from Proof Failures in SPARK. SEFM 2016: 215-233 - 2015
- [j4]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): 695-707 (2015) - 2014
- [c6]Johannes Kanig, Roderick Chapman
Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification. TAP@STAF 2014: 142-157 - 2013
- [j3]Yannick Moy, Emmanuel Ledinot, Hervé Delseny, Virginie Wiels, Benjamin Monate:
Testing or Formal Verification: DO-178C Alternatives and Industrial Experience. IEEE Softw. 30(3): 50-57 (2013) - 2012
- [c5]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: 49-59 - [c4]Cyrille Comar, Johannes Kanig, Yannick Moy:
Integration von Formaler Verifikation und Test. Automotive - Safety & Security 2012: 133-148 - [c3]Maria-Virginia Aponte, Pierre Courtieu, Yannick Moy, Marc Sango:
Maximal and Compositional Pattern-Based Loop Invariants. FM 2012: 37-51 - 2011
- [j2]Johannes Kanig, Jérôme Guitton, Yannick Moy:
Hi-Lite - Verification by Contract. Softwaretechnik-Trends 31(3) (2011) - [c2]Claire Dross, Jean-Christophe Filliâtre, Yannick Moy:
Correct Code Containing Containers. TAP@TOOLS 2011: 102-118 - 2010
- [j1]Yannick Moy, Claude Marché:
Modular inference of subprogram contracts for safety checking. J. Symb. Comput. 45(11): 1184-1211 (2010)
2000 – 2009
- 2008
- [c1]Yannick Moy:
Sufficient Preconditions for Modular Assertion Checking. VMCAI 2008: 188-202
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from ,
, and
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and
to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-05-08 21:49 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by: