Go to file
Frédéric Bour 7c6ff8db19 Extend logical sequences, begin formalisation of arrays 2021-12-31 15:44:29 +01:00
attic add attic 2020-03-19 10:36:00 +01:00
congre Restructure repository 2021-03-30 11:10:02 +02:00
doc Typos in zml.md 2021-11-29 22:38:02 +01:00
zml Extend logical sequences, begin formalisation of arrays 2021-12-31 15:44:29 +01:00
ztl Minor cleanup 2021-12-27 14:09:21 +01:00
.gitignore Emacs mode 2020-02-05 14:57:34 +01:00
Makefile Typos in zml.md 2021-11-29 22:38:02 +01:00
README.md Correction des liens dans le README 2021-12-31 15:43:05 +01:00
dune-project Emacs mode 2020-02-05 14:57:34 +01:00
zml.opam initial import 2020-01-23 16:47:33 +01:00

README.md

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).