Logiciels

Le laboratoire essaye dans la mesure du possible de rendre disponibles les logiciels qu’il produit sous la forme de logiciels libres. Ces logiciels sont identifiés par un badge qui mentionne leur licence libre.

L’usage d’une licence libre a pour but de faciliter la diffusion des résultats de nos recherches dans le monde académique et plus généralement dans notre société numérique. C’est aussi un moyen pour le laboratoire de partager l’effort de maintenance des outils et bibliothèques qu’il conçoit pour ses besoins internes. Ces logiciel sont souvent disponibles « en développement ouvert », sur le compte github du laboratoire ou une autre plateforme de développement collaboratif.

Software
  • LGPL

Un plugin eclipse pour le langage de specification Alloy 4.

Software

Un solveur rapide pour l'argumentation abstraite basé sur les contraintes

CP

CPT est un planificateur temporel.

LS

LSAT est un solveur SAT basé sur la procédure classique DPLL à laquelle a été ajouté un pré-traitement permettant de récupérer et d’exploiter les informations structurelles cachées par la forme normale conjonctive.

Ma

ManySat est un solveur parallèle de type DPLL incluant toute les fonctionnalités des solveurs SAT modernes (analyse de conflits, heuristique basée sur les activités, etc.) et celles issues de nos résultats récents sur l’amélioration des techniques d’analyse de conflits.

Op

OpenQBF est un prouveur QBF en Java simple mais correct. Il n’est plus maintenu depuis 2004. Le code source du prouveur est disponible sur sourceforge.

Pe

La résolution parallèle de SAT basée sur le LBD et le PSM.

pp
  • GPL

Le solveur SAT aux 16 médailles à la compétition SAT de 2011

PR
  • GPL

PRISM est l'acronyme de Platform for Reasoning with Inconsistency Shapley Measure.

QB

QBFL est un prouveur QBF prenant avantage des classes polynomiales de ce problème.

Re

ReViVal est une technique de simplification (ou de vivification) de formules CNF.

Va

valCSP est un solveur de réseaux de contraintes (formalisme CSP). Il s’intéresse aux problèmes de décision liés aux CSP.

Wo

Woodstock est un solveur de jeux pour le General Game Playing basé sur les CSP stochastiques.

YA

YAHSP est un planificateur par recherche heuristique pour la planification classique sous horizon borné.