Skip to content
Snippets Groups Projects
Commit a3145c5c authored by Pierre Courtieu's avatar Pierre Courtieu
Browse files

Merge branch 'vapontegarcia-master-patch-27302' into 'master'

Update codemeta.json

See merge request xurbain/pactole-dev!4
parents 522f1b43 5761ce88
No related branches found
No related tags found
No related merge requests found
{
"@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"
}
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