OCamlPro started working on blockchains in 2014, when Arthur Breitman came to us with an initial idea to develop the Tezos ledger. The idea was very challenging with a lot of innovations. So, we collaborated with him to write a specification, and to turn the specification into OCaml code. Since then, we continually improved our skills […]
Author: Mohamed Iguernlala
After the hard work done on the integration of floating-point arithmetic reasoning two years ago, 2018 is the year of polymorphic SMT2 support and efficient SAT solving for Alt-Ergo. In this post, we recap the main novelties last year, and we announce the first Alt-Ergo Users’ Club meeting. An SMT2 front-end with prenex polymorphism As […]
Categories
Release of Alt-Ergo 2.2.0
A new release of Alt-Ergo (version 2.2.0) is available. You can get it from Alt-Ergo’s website. An OPAM package for it will be published in the next few days. The major novelty of this release is a new experimental front-end that supports the SMT-LIB 2 language, extended prenex polymorphism. This extension is implemented as a […]
Categories
Release of Alt-Ergo 2.1.0
A new release of Alt-Ergo (version 2.1.0) is available on Alt-Ergo’s website: https://alt-ergo.ocamlpro.com/#releases. An OPAM package for it will be published soon. In this release, we mainly improved the CDCL-based SAT solver to get performances similar to/better than the old Tableaux-like SAT. The CDCL solver is now the default Boolean reasoner. The full list of […]
We have recently released a new (public up-to-date) version of Alt-Ergo. We focus in this article on its main new feature: experimental support for models generation. This work has been done with Frédéric Lang, an intern at OCamlPro from February to July 2016. The idea behind models generation The idea behind this feature is the […]
Categories
Private Release of Alt-Ergo 1.00
After the public release of Alt-Ergo 0.99.1 last December, it’s time to announce a new major private version (1.00) of our SMT solver. As usual: we freely provide a JavaScript version on Alt-Ergo’s website, we provide a private access to our internal repositories for academia users and our clients. Quick Evaluation A quick comparison between […]
Categories
Try Alt-Ergo in Your Browser
Recently, we worked on an online Javascript-based serverless version of the Alt-Ergo SMT solver. In what follows, we will explain the principle of this version of Alt-Ergo, show how it can be used on a realistic example and compare its performances with bytecode and native binaries of Alt-Ergo. Compilation “Try Alt-Ergo” is a Javascript-based version […]
Categories
Alt-Ergo @ OCamlPro: Two months later
As announced in a previous post, I joined OCamlPro at the beginning of September and I started working on Alt-Ergo. Here is a report presenting the tool and the work we have done during the two last months. Alt-Ergo at a Glance Alt-Ergo is an open source automatic theorem prover based on SMT technology. It […]
RECENT POSTS
- A Dune Love story: From Liquidity to Love
- [Interview] Sylvain Conchon joins OCamlPro
- A Solidity parser in OCaml with Menhir
- opam 2.0.7 release
- opam 2.1.0 alpha is here!
- An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy
- New version of Try OCaml in beta!
- Alt-Ergo Users’ Club Annual Meeting
- 2019 at OCamlPro
- opam 2.0.6 release
RECENT COMMENTS
- Muriel Shan Sei Fan - [Interview] Sylvain Conchon joins OCamlPro
- Yannick Moy - [Interview] Sylvain Conchon joins OCamlPro
- [Interview] Sylvain Conchon joins OCamlPro - OCamlPro - An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy
- Blockchains @ OCamlPro: an Overview - OCamlPro - Improving Tezos Storage : Gitlab branch for testers
- The Opam 2.0 cheatsheet, with a new theme! – OCamlPro - Updated Cheat Sheets: OCaml Language and OCaml Standard Library
- Better Inlining: Progress Report – OCamlPro - Optimisations you shouldn’t do
- An Indentation Engine for OCaml – OCamlPro - An Overview of our Current Activities
- An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy | Chris Short - An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy
- Thomas Blanc - An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy
- nbbb - An in-depth Look at OCaml’s new “Best-fit” Garbage Collector Strategy