Skip to content
Snippets Groups Projects
Commit fa70e060 authored by Virginia Aponte Garcia's avatar Virginia Aponte Garcia
Browse files

Update codemeta.json

parent 344d8760
No related branches found
No related tags found
No related merge requests found
{ {
"@context": "https://doi.org/10.5063/schema/codemeta-2.0", "@context": "https://w3id.org/codemeta/3.0",
"@type": "SoftwareSourceCode", "type": "SoftwareSourceCode",
"name": "Pactole", "applicationCategory": "Coq library dedicated to formal verification of mobile robotic swarm distributed protocols",
"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"
],
"author": [ "author": [
{ {
"@type": "Person", "id": "https://orcid.org/0000-0001-8789-9781",
"@id": "https://orcid.org/0000-0001-8789-9781", "type": "Person",
"givenName": "Pierre",
"familyName": "Courtieu",
"email": "Pierre.Courtieu@lecnam.net",
"affiliation": { "affiliation": {
"@type": "Organization", "type": "Organization",
"name": "Conservatoire National des Arts et Métiers" "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",
"@id": "https://orcid.org/0000-0001-7442-2538", "type": "Person",
"givenName": "Xavier",
"familyName": "Urbain",
"email": "Xavier.Urbain@univ-lyon1.fr",
"affiliation": { "affiliation": {
"@type": "Organization", "type": "Organization",
"name": "Université Claude Bernard Lyon 1" "name": "Université Claude Bernard Lyon 1"
} },
} "email": "Xavier.Urbain@univ-lyon1.fr",
"familyName": "Urbain",
"givenName": "Xavier"
},
{ {
"@type": "Person", "id": "_:author_3",
"givenName": "Lionel", "type": "Person",
"familyName": "Rieg",
"email": "lionel.rieg@univ-grenoble-alpes.fr",
"affiliation": { "affiliation": {
"@type": "Organization", "type": "Organization",
"name": "Verimag, Grenoble INP -- UGA" "name": "Verimag, Grenoble INP -- UGA"
} },
"email": "lionel.rieg@univ-grenoble-alpes.fr",
"familyName": "Rieg",
"givenName": "Lionel"
} }
], ],
"contributor": "TODO: Les stagiaires comme ci-dessus?", "codeRepository": "https://gitlab.liris.cnrs.fr/pactole/coq-pactole",
"citation": "TODO un papier décrivant 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.0",
"developmentStatus": "active",
"funding": "Digiteo Project #2009-38HD, ANR Project 2019-CE25-0005",
"referencePublication": "https://doi.org/10.4230/LITES.8.2.2"
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment