Olive - OCaml Integrated Verification Environment

Organisation du dépôt

• zml est le projet principal, pour l'instant un mini-ml avec une logique intégrée
• ztl est une couche au-dessus de Z3 qui offre une API typée et une API pure
• congre est une implémentation d'un algorithme de congruence closure, adapté au besoin de zml.

Installation

Une fois le dépôt cloné, il faudra installer z3, menhir, pprint et grenier (> 0.12):

opam install z3 menhir pprint grenier

Test

Lancer make depuis le répertoire racine va construire le driver (point d'entrée: zml/bin/main.ml)

Frontend emacs

Le dossier zml/ contient des morceaux d'un mode emacs qui n'est pas du tout à jour, il ne faut pas l'utiliser (en tout cas pour l'instant).