Explore projects

implementation and metatheory of time credits and time receipts in Iris / Coq

An SQL querybuilder written in Python.

Python API and schedulers for Batsim

Separation Logic with Characteristic Formulae Entirely within Coq

Why3 is a software verification platform, featuring a versatile ML-style language and interfaces to various powerful automated and interactive theorem provers.

FLoRaSat (Framework for LoRa-based Satellite networks) is an Omnet++ based discrete-event simulator to carry out end-to-end satellite IoT simulations based on LoRa and LoRaWAN adaptations to the space domain.

Heuristics for Heterogeneous Memory (H2M) - Runtime Library & Examples

An actor library for OCaml 5

Itauto: an Extensible Intuitionistic SAT Solver

Itauto: an Extensible Intuitionistic SAT Solver

C library for fft in double precision with bounded error

Music transcription framework based on parsing for weighted regular tree grammars

Coherent predicates: translation validation of properties of various types of predicates at runtime, interfacing with SMTCoq for validation of SMT unsatisfiability certificates.

Primary library for necro, and standard tools (parse, print and compil)

A Unified Runtime System for Heterogeneous Multicore Architectures.

More informations on https://starpu.gitlabpages.inria.fr/

Package for graph and mesh/hypergraph partitioning, graph clustering, and sparse matrix ordering.