Categories

[Interview] Sylvain Conchon joins OCamlPro

On April 2020, Sylvain Conchon joined the OCamlPro team as our Chief Scientific Officer on Formal Methods. Sylvain is a professor at University Paris-Saclay, he has also been teaching OCaml in universities for about 20 years. He is the co-author of Apprendre à programmer avec OCaml with Jean-Christophe Filliâtre, a book for students in French […]

Categories

Alt-Ergo Users’ Club Annual Meeting

The second annual meeting of the Alt-Ergo Users’ Club was held in mid-February. Our annual meeting is the perfect place to review each partner’s needs regarding Alt-Ergo. This year, we had the pleasure of receiving our partners to discuss the roadmap for future Alt-Ergo developments and enhancements. Alt-Ergo is an automatic mathematical formula checker, jointly […]

2019 at OCamlPro

OCamlPro was created to help OCaml and formal methods spread into the industry. We grew from 1 to 21 engineers, still strongly sharing this ambitious goal! The year 2019 at OCamlPro was very lively, with fantastic accomplishments all along! Let’s quickly review the past years’ works, first in the world of OCaml (flambda2 & compiler optimisations, […]

Categories

The Alt-Ergo SMT Solver’s results in the SMT-COMP 2019

The results of the SMT-COMP 2019 were released a few days ago at the SMT whorkshop during the 22nd SAT conference. We were glad to participate in this competition for the second year in a row, especially as Alt-Ergo now supports the SMT-LIB 2 standard. Alt-Ergo is an open-source SAT-solver maintained and distributed by OCamlPro […]

Categories

What’s new for Alt-Ergo in 2018 ? Here is a recap !

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.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 […]

2017 at OCamlPro

Since 2017 is just over, now is probably the best time to review what happened during this hectic year at OCamlPro… Here are our big 2017 achievements, in the world of blockchains (the Liquidity smart contract language, Tezos and the Tezos ICO,  etc.), of OCaml (with OPAM 2, flambda 2 etc.), and of formal methods […]

Categories

Release of Alt-Ergo 1.30 with experimental support for models generation

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 […]

Reduced Memory Allocations with ocp-memprof

In this blog post, we explain how ocp-memprof helped us identify a piece of code in Alt-Ergo that needed to be improved. Simply put, a function that merges two maps was performing a lot of unnecessary allocations, negatively impacting the garbage collector’s activity. A simple patch allowed us to prevent these allocations, and thus speed […]