Logiciel Année : 2025

Pactole

Pierre Courtieu
CEDRIC. Systèmes sûrs
Conservatoire National des Arts et Métiers [CNAM]
CV
Xavier Urbain
Laboratoire d'InfoRmatique en Image et Systèmes d'information
Lionel Rieg
  • Fonction : Auteur
  • PersonId : 1123946
VERIMAG

Résumé

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.

Domaines

Calcul parallèle, distribué et partagé [cs.DC] Logique en informatique [cs.LO]
DOI

Cite 10.4230/LITES.8.2.2 Swarms of Mobile Robots: Towards Versatility with Safety, https://doi.org/10.4230/lites.8.2.2

Pierre Courtieu  : Connectez-vous pour contacter le contributeur

https://cnam.hal.science/hal-04911413

Soumis le : vendredi 24 janvier 2025-17:43:25

Dernière modification le : mercredi 29 janvier 2025-03:29:52

Consulter sur Present sur SoftwareHeritage

Dates et versions

hal-04911413 , version 1 (24-01-2025)

Identifiants

Métadonnées

  • version : 2.1
  • softwareLicence : https://spdx.org/licenses/LGPL-3.0
  • programmingLanguage : Coq , Rocq
  • codeRepository : https://gitlab.liris.cnrs.fr/pactole/coq-pactole
  • runtimePlatform : Coq-8.20

Citer

Exporter

CodeMeta BibTeX XML-TEI Dublin Core DC Terms EndNote DataCite

Collections

UGA IMAG CNRS UNIV-LYON1 UNIV-LYON2 INSA-LYON EC-LYON CNAM LIRIS VERIMAG INSA-GROUPE CEDRIC-CNAM UDL ANR HESAM
0 Consultations
0 Téléchargements

Partager

More