Articles tagged with alt-ergo


Authors: OCamlPro
Date: 2021-04-29
Category: Formal Methods
Tags: alt-ergo, fr

La troisième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu le 1er avril ! Cette réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Nous avons eu le plaisir de recevoir nos partenaires pour discuter de la feuille de... (Read more)

Authors: Albin Coquereau
Date: 2021-03-29
Category: Formal Methods
Tags: alt-ergo

Have you heard about our Try-Alt-Ergo website? Created in 2014 (see our blogpost), the first objective was to facilitate access to our performant SMT Solver Alt-Ergo. Try-Alt-Ergo allows you to write and run your problems in your browser without any server computation. This playground website has be... (Read more)

Authors: Albin Coquereau
Date: 2021-01-22
Category: Formal Methods
Tags: alt-ergo

A new release of Alt-Ergo (version 2.4.0) is available. You can get it from Alt-Ergo's website. The associated opam package will be published in the next few days. This release contains some major novelties: Alt-Ergo supports incremental commands (push/pop) from the smt-lib standard. We switched co... (Read more)

Authors: Aurore Dromby
Date: 2020-03-03
Category: Formal Methods
Tags: alt-ergo, fr

Alt-Ergo meeting Logo Alt-Ergo La deuxième réunion annuelle du Club des utilisateurs d’Alt-Ergo a eu lieu à la mi-février ! Notre réunion annuelle est l’endroit idéal pour passer en revue les besoins de chaque partenaire concernant Alt-Ergo. Cette année, nous avons eu le plaisir de recevo... (Read more)

Authors: OCamlPro
Date: 2020-02-04
Category: OCamlPro

2019 at OCamlPro OCamlPro a pour ambition d’aider les industriels dans leur adoption du langage OCaml et des méthodes formelles. L’entreprise est passée d’1 à 21 personnes et est restée fidèle à cet objectif. L’année 2019 chez OCamlPro a été très animée, et le nombre de réalisati... (Read more)

Authors: Albin Coquereau
Date: 2019-07-10
Category: Formal Methods
Tags: alt-ergo, fr

Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop  SMT de la 22e conférence SAT. Nous étions fiers d’y participer pour la deuxième année consécutive, surtout depuis qu’Alt-Ergo prend en charge le standard SMT-LIB 2. Alt-Ergo est un SAT solveur open-source main... (Read more)

Authors: Albin Coquereau
Date: 2019-07-10
Category: Formal Methods
Tags: alt-ergo

Les résultats de la compétition SMT-COMP 2019 ont été publiés au whorkshop SMT de la 22e conférence SAT. Nous étions fiers d’y participer pour la deuxième année consécutive, surtout depuis qu’Alt-Ergo prend en charge le standard SMT-LIB 2. Alt-Ergo est un SAT solveur open-source mainte... (Read more)

Authors: Albin Coquereau
Date: 2019-07-09
Category: Formal Methods
Tags: alt-ergo

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 maintaine... (Read more)

Date: 2019-02-11
Category: Formal Methods
Tags: alt-ergo

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 SMT... (Read more)

Authors: Muriel, OCamlPro
Date: 2019-02-04
Category: OCamlPro

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... (Read more)

Date: 2018-04-23
Category: Formal Methods
Tags: alt-ergo

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 ex... (Read more)

Date: 2018-03-14
Category: Formal Methods
Tags: alt-ergo

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. Th... (Read more)

Authors: Muriel
Date: 2018-01-15
Category: 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 ... (Read more)

Date: 2016-11-21
Category: Formal Methods
Tags: alt-ergo

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... (Read more)

Date: 2015-01-29
Category: Formal Methods

altergo logo 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 o... (Read more)

Authors: Çagdas Bozman
Date: 2014-07-16
Category: OCamlPro

Here is a short report on some of our public activities in May and June 2014. Towards OPAM 1.2 After a lot of discussions and work on OPAM itself, we are now getting to a clear workflow for OCaml developpers and packagers: the preliminary document for OPAM 1.2 is available here. The idea is that you... (Read more)

Date: 2014-07-15
Category: Formal Methods

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. Comp... (Read more)

Date: 2013-10-02
Category: Formal Methods
Tags: alt-ergo

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 technol... (Read more)