diff --git a/codemeta.json b/codemeta.json
index de545b51aa98ebf74a62f91069fbf722824202a4..d6ace5d8e2dd34759b9a802fc172a18d720d908a 100644
--- a/codemeta.json
+++ b/codemeta.json
@@ -1,69 +1,57 @@
{
- "@context": "https://doi.org/10.5063/schema/codemeta-2.0",
- "@type": "SoftwareSourceCode",
- "name": "Pactole",
- "license": "https://spdx.org/licenses/LGPL-3.0",
- "codeRepository": "https://gitlab.liris.cnrs.fr/pactole/coq-pactole",
- "relatedLink": "TODO? https://???",
- "dateCreated": "TODO 2013-??-??",
- "datePublished": "TODO 2024-???",
- "version": "TODO 2.0???",
- "description": "TODO A Coq library formalizing the distributed computing model for robot swarm called Look-Compute-Move (due to Suzuki and Yamashita) and several case studies in this model. ",
- "applicationCategory": "FIXME: Formal development",
- "releaseNotes": "TODO Second release.",
- "runtimePlatform": "Coq-8.20",
- "developmentStatus": "active",
- "funding": [
- { "@type":"Grant",
- "identifier": "Digiteo Project #2009-38HD" } ,
- { "@type":"Grant",
- "identifier": "ANR Project 2019-CE25-0005" }
- ],
- "keywords": [
- "distributed systems",
- "formal proof",
- "robot swarm"
- ],
- "programmingLanguage": [
- "Coq/Rocq"
- ],
- "runtimePlatform": [
- "Coq/Rocq"
- ],
+ "@context": "https://w3id.org/codemeta/3.0",
+ "type": "SoftwareSourceCode",
+ "applicationCategory": "Coq library dedicated to formal verification of mobile robotic swarm distributed protocols",
"author": [
{
- "@type": "Person",
- "@id": "https://orcid.org/0000-0001-8789-9781",
- "givenName": "Pierre",
- "familyName": "Courtieu",
- "email": "Pierre.Courtieu@lecnam.net",
+ "id": "https://orcid.org/0000-0001-8789-9781",
+ "type": "Person",
"affiliation": {
- "@type": "Organization",
+ "type": "Organization",
"name": "Conservatoire National des Arts et Métiers"
- }
+ },
+ "email": "Pierre.Courtieu@lecnam.net",
+ "familyName": "Courtieu",
+ "givenName": "Pierre"
},
{
- "@type": "Person",
- "@id": "https://orcid.org/0000-0001-7442-2538",
- "givenName": "Xavier",
- "familyName": "Urbain",
- "email": "Xavier.Urbain@univ-lyon1.fr",
+ "id": "https://orcid.org/0000-0001-7442-2538",
+ "type": "Person",
"affiliation": {
- "@type": "Organization",
+ "type": "Organization",
"name": "Université Claude Bernard Lyon 1"
- }
- }
+ },
+ "email": "Xavier.Urbain@univ-lyon1.fr",
+ "familyName": "Urbain",
+ "givenName": "Xavier"
+ },
{
- "@type": "Person",
- "givenName": "Lionel",
- "familyName": "Rieg",
- "email": "lionel.rieg@univ-grenoble-alpes.fr",
+ "id": "_:author_3",
+ "type": "Person",
"affiliation": {
- "@type": "Organization",
+ "type": "Organization",
"name": "Verimag, Grenoble INP -- UGA"
- }
+ },
+ "email": "lionel.rieg@univ-grenoble-alpes.fr",
+ "familyName": "Rieg",
+ "givenName": "Lionel"
}
],
- "contributor": "TODO: Les stagiaires comme ci-dessus?",
- "citation": "TODO un papier décrivant Pactole"
+ "codeRepository": "https://gitlab.liris.cnrs.fr/pactole/coq-pactole",
+ "description": "A Coq library dedicated to formally verifying distributed protocols for mobile robot swarms. The library implements various extensions of the Look-Compute-Move model, first proposed by Suzuki and Yamashita, providing a robust framework for protocol verification in different theoretical settings. ",
+ "keywords": [
+ "distributed systems",
+ "deductive verification",
+ "formal proof",
+ "robotic swarms"
+ ],
+ "license": "https://spdx.org/licenses/LGPL-3.0",
+ "name": "Pactole",
+ "programmingLanguage": "Coq/Rocq",
+ "relatedLink": "https://pactole.liris.cnrs.fr/",
+ "runtimePlatform": "Coq-8.20",
+ "version": "2.1",
+ "developmentStatus": "active",
+ "funding": "Digiteo Project #2009-38HD, ANR Project 2019-CE25-0005",
+ "referencePublication": "https://doi.org/10.4230/LITES.8.2.2"
}