OCamlPro/alt-ergo

Stars
133
Rank 272,600 (Top 6 %)
Language
OCaml
License
Other
Created almost 11 years ago
Updated 23 days ago

OCamlPro/alt-ergo

OCamlPro

There are no reviews yet. Be the first to send feedback to the community and the maintainers!

OCamlPro public development repository for Alt-Ergo

Alt-Ergo

Alt-Ergo is an open-source automatic solver of mathematical formulas designed for program verification. It is based on Satisfiability Modulo Theories (SMT). Solvers of this family have made impressive advances and became very popular during the last decade. They are now used is various domains such as hardware design, software verification and formal testing. It was developed at LRI, and is now improved and maintained at OCamlPro, and friendly collaboration is maintained with the Why3 development team.

You can try Alt-Ergo online. Also see the Alt-Ergo Users' Club.

Build status

next	main

Website

Alt-Ergo's website: https://alt-ergo.ocamlpro.com.

Documentation

See our general documentation wich contains

installing informations
the usage section for information on how to use Alt-Ergo.
A section about input file format supported by Alt-Ergo.
API and developers documentation.

Download

We provide sources tarball of the latest release of Alt-Ergo. You can also find it on the GitHub's releases' page.

Alt-Ergo is available in the OCaml package manager opam with this command:

opam install alt-ergo

Copyright

Alt-Ergo is freely available for non-commercial uses (such as academic and exploratory trials) under the OCamlPro non-commercial license 1.0.

For commercial use, see the Alt-Ergo Users' Club. Club members with adequate membership can have access to Alt-Ergo under the Apache Software License version 2.0. See the license section for more detail.

Build

See installing informations section.

Contributing

Please refer to our contributing guidelines.

Support

See Alt-Ergo @ OCamlPro or contact us at [email protected] for more details.

ocp-indent

Indentation tool for OCaml, to be used from editors like Emacs and Vim.

drom

drom is a wrapper over opam/dune in an attempt to provide a cargo-like user experience. It can be used to create full OCaml projects with sphinx and odoc documentation. It has specific knowledge of Github and will generate files for Github Actions CI and Github pages.

liquidity

A high-level language for Dune Network (and Tezos) with OCaml and ReasonML syntaxes, with a decompiler from Michelson

ocaml-cheat-sheets

OCaml Documentations as one-pagers, easy to keep useful commands in mind

owi

WebAssembly Swissknife & cross-language bugfinder

ollvm

An higher-level LLVM binding for OCaml

tryocaml

An interactive tutorial to begin learning with OCaml

dirdiff

Efficiently compute the differences between two directories

ocaml-top

A simple cross-platform OCaml code editor built for top-level evaluation.

ocp-index

Easy access to the interface information of installed OCaml libraries for editors like Emacs and Vim.

ocaml-canvas

The OCaml-Canvas library provides a portable Canvas for OCaml

wasocaml

numcaml

Scientific Computing Tools For OCaml

directories

directories is an OCaml library that provides configuration, cache and data paths (and more!) following the suitable conventions on Linux, macOS and Windows. The following conventions are used: XDG Base Directory Specification and xdg-user-dirs on Linux, Known Folders on Windows, Standard Directories on macOS.

ocpwin-distrib

Knowledge Database for OCamlPro's version of OCaml on Windows

ocaml-solidity

Ocaml-solidity provides a Solidity parser and typechecker

OCamlPro-OCaml-Branch

This is a fork of the inline-more branch in the OCaml SVN repository.

wxOCaml

a WxWidgets binding for OCaml

memthol

Memthol is a visualizer for memory profiling data generated from OCaml programs.

ocplib-json-typed

Libraries for reliable manipulation JSON objects.

ocb

ocb (OCaml Badgen) is an OCaml library for SVG badge generation. There's also a command-line tool provided.

mikino_bin

A simple induction and BMC engine.

ocp-ocamlres

A simple tool and library to embed files and directories inside an OCaml executables

typerex-lint

Tools to manipulate source files (linting, patching, etc.)

ez_api

Easily build clients and servers on top of a common REST API, automatically derived from OCaml types.

techelson

A test execution engine for Michelson smart contracts.

opam-bin

Binary packages for OPAM with local and remote repositories

ocplib-resto

A minimal OCaml library for type-safe HTTP/JSON RPCs

freeton_wallet

The 'ft' tool is a multi-account terminal wallet for the Free TON blockchain. It is based on the freeton_ocaml_sdk.

ezjs

Some useful libraries to work with `js_of_ocaml`

optal

A new language for optimization

ocplib-endian

Optimised functions to read and write int16/32/64 from strings, bytes and bigarrays, based on primitives added in version 4.01.

agrid

agrid is an OCaml library for adjustable grids. Adjustable grids are two dimensional arrays whose width/height can be changed by adding or removing row/column at either end (one at a time).

ez_cmdliner

flambda-task-force

ocplib-simplex

A library implementing a simplex algorithm, in a functional style, for solving systems of linear inequalities

tzscan

The TzScan block explorer for Tezos

socaml-analyzer

ocamlexc

OCaml uncaught exception analyser

digodoc

Dig into an opam switch for doc

scilint

A tool to analyze Scilab projects to find potential bugs

opam-manager

SecurOCaml

Repository of the SecurOCaml Project

ocaml-perf

binding for linux-perf library for OCaml

matla

A manager for TLA+ projects, written in Rust.

freeton_ocaml_sdk

A binding to the Everscale Rust library from OCaml.

relocation-patches

A repository of patches to make OPAM packages relocatable

ocp-typechecker

A tool to verify types inferred by OCaml

operf-micro

A set of micro-benchmarks for OCaml compiler

ezjs_fetch

Bindings for Fetch

opam-wix

opam-wix is opam plugin that creates msi installation file to install packages and binaries on Windows.

ez_pgocaml

ezjs_min

A bunch of js_of_ocaml shortcuts

ez_search

Simple module to search in a set of files

operf-macro

Some macro-benchmarks for operf and an OPAM repository for them

typerex-lldb

An OCaml binding to the LLDB Debugging Framework

ocaml-benchs

Sources of the set of benchmarks distributed in OCamlPro/opam-bench-repo

ows

A service to analyse the state of the opam repository w.r.t. all available version of the OCaml compiler.

ocp-build

See www.typerex.org to download ocp-build

ocplib-i18n

ocp-reveal

An OCaml binding for reveal.js, a html presentation framework.

ez_file

Library with helpers to manipulate files, read/write their content, search directories, etc.

opam-builder

ocamltk

the initial ocaml tk library

jit_ocaml

A JIT in OCaml for Scilab (part of the Richelieu FUI project)

ez_opam_file

a compatibility library for opam-file-format

ezjs_ace

Bindings for the Ace editor

typerex-attic

A set of simple tools and libraries that we developed over the years for temporary OCaml projects. Most of them are only maintained/improved when we need them for a task.

ISN-OCaml

Les exemples de code de l'option ISN (Informatique & Sciences du Numérique) en OCaml

ocp-reloc

OCaml bytecode relocation

liq_game

richelieu

OCamlPro working copy of the Richelieu branch of Scilab 6

verification_for_dummies

Induction as a formal program verification technique for the uninitiated, written in Rust.

ez_config

Library to read/write configuration files in OCaml syntax

ocamlbench-repo

An opam 2.0 repository holding the definition for benches on bench.flambda.ocamlpro.com

perfOCaml-2014

an environment to evaluate the performance of OCaml compilers and programs

ez_text_renderer

ocplib-cmi

Small library to work with OCaml cmi files

ez_subst

Simple substitution module for OCaml

ocaml-materialize

Javascript Binding on Materialize

niagara-lang

Compiler for the Niagara language

superbol-vscode-extension

A VSCode extension for COBOL

cargo-graph

Display a graph from the Cargo packages in a Rust project

ocplib_stuff

This library contains some basic stuff that is used in some OCP libraries and applications. Most of them are probably available in other extensions of the standard libraries (extlib, core, etc.), but we are used to these ones.

ocamlc-plugins

Examples of plugins for ocamlc/ocamlopt

ezjs_blockies

Bindings for Blockies

www.freeton.link

A directory of resources on Free TON

ezjs_recaptcha

OCaml bindings for reCAPTCHA

opam-bin-repository

Repository for `opam-bin`

ucf-rddl

ezjs_cleave

OCaml bindings for Cleave JS

ezjs_idb

Js_of_ocaml bindings for IndexedDB

ezjs_d3pie

OCaml bindings for d3pie

swhid_core

ocp-cplugins

Collection of plugins for CAML_CPLUGINS

opam-bench-repo

Set of benchmarks for OCaml organized as an OPAM repository

ezjs_push

OCaml bindings for Push Notification

swhid

swhid is an OCaml library to work with persistent identifiers found in Software Heritage, also known as swhid

ezjs_qrcode

OCaml bindings for QRCode.js

opam-custom-install

An opam plugin to install a package using a custom command