"own"

Formal Verification of Critical Aerospace Software

A Generic Ellipsoid Abstract Domain for Linear Time Invariant Systems

CAVALE - Intégration dans les processus de validation - focus sur les propriétés fonctionnelle. RF 4/14888

Incremental verification with mode variable invariants in state machines

Invariant stream generators using automatic abstract transformers based on a decidable logic

Kind,a k-induction based model-checker

Kind-AI, automatic abstract interpreter module for Lustre model-checker Kind

LustreC: a modular Lustre compiler

Ocaml library for Semi-Definite Programming (SDP, SOS)

PVS Linear Algebra Libraries for Verification of Control Software Algorithms in C/ACSL