Welcome to the FoCaLiZe website. This site offers information about FoCaLiZe, some documentation about the language and its compiler, some training opportunities, and of course, the latest release of FoCaLiZe.

Overview

The FoCaLiZe project aims at providing a programming environment to develop certified programs. The environment is based on a functional programming language with object-oriented features. The language allows the programmer to write formal specifications and proofs of the program in a unified and consistent setting.

From a FoCaLiZe source code development, the focalizec compiler produces three source files:

Thanks to built-in inheritance mechanisms, the language allows to refine a development from the coarse-grain specification to the fully defined executable program.

Proofs are written in a hierarchical style in the FoCaLiZe Proof Language and are then independent from the target logical verification system. Leaves of a proof tree are solved by providing "hints" (definition, theorem, proof step etc. names) which are sent to the Zenon automatic theorem prover.

The FoCaLiZe distribution includes a library of mathematical algebraic structures up to multivariate polynomial rings, a library of security policies and various examples contributed by FoCaLiZe users. The resulting libraries are noticeably efficient; for instance, the complex algorithms of the algebraic library provide runtime performances comparable to the best Computer Algebra Systems available.

FoCaLiZe is developped by François Pessaux. Zenon is developped by Damien Doligez.

New release (0.9.5) of the FoCaLiZe environment (2023-05-22)

The new release of the FoCaLiZe environment, focalize 0.9.5, is now available.
After being broken for a long time due to changes in OCaml and Coq, this version is now compatible with the recent versions of OCaml (5.0.0) and Coq (8.17.0). As a side effect, this makes FoCaLiZe available on Mac Silicon (M1/M2).
The distribution is available from the dedicated GitHub repository.

New release (0.9.2) of the FoCaLiZe environment (2018-09-03)

The new release of the FoCaLiZe environment, focalize 0.9.2, is now available. As for previous releases, some bugs have been fixed in the focalizec compiler.
This version introduces the Dedukti backend written by Raphaël Cauderlier, taking benefits from Zenon_modulo to ease proofs.
The Coq backend now generates Coq code compatible with Coq 8.8. A complete description of changes / new features can in found in the CHANGES file of the distribution.

Git migration to GitHub (2018-08-07)

FoCaLiZe git repository moved to GitHub. You may find the project page and clone the repository from https://github.com/pessaux-f/focalize.git.

FAQ started (2017-03-03)

A currently short but growing FAQ about common errors is now available from the Documentation page.

Zenon (0.8.2) available (2016-06-06)

Bugs have been fixed for proofs using definitions of recursive functions, and some proofs using congruence-related mechanisms. This version is available from its GIT repository or Zenon website.

Zenon (0.8.1) available (2016-05-31)

A minor change in Zenon installation process allowing to handle Coq 8.5 has been made. This version is available from its GIT repository or Zenon website.

New release (0.9.1) of the FoCaLiZe environment (2016-05-30)

The new release of the FoCaLiZe environment, focalize 0.9.1, is now available. A certain number of bugs found in the focalizec compiler have been fixed. The generated code is slightly lighter. Termination proofs for recursive functions, in addition to the previously available structural way, can be now written using a measure or a well-founded relation. The generated Coq code is now compatible with Coq 8.5, but whoever requires Zenon 8.0.1 (or to configure its installation to store the libraries in a dedicated directory). A complete description of changes / new features can in found in the CHANGES file of the distribution.

Experimental mirror of GIT repositories (Nov 2014)

The GIT repositories of FoCaLiZe and Zenon are now daily mirrored at ENSTA. We hope that the synchronization will work fine...

New release (0.9.0) of the FoCaLiZe environment (2014-10-14)

The new release of the FoCaLiZe environment, focalize 0.9.0, is now available. A certain number of bugs found in the focalizec compiler have been fixed and Zenon also had several issues fixed. Final let-definitions are now integrated. The computation of dependencies has been deeply rewritten to compute them *once* for all the possible backends (OCaml, Coq). Generated code is slightly lighter and naming schemes and code generation schemes have been standardized between OCaml and Coq. A complete description of changes / new features can in found in the CHANGES file of the distribution.

Server issue and migration (Sept-Oct 2014)

Due to an issue on the old server hosting FoCaLiZe, the site was down during some weeks. The situation is now back to a normal state after a migration. Only the bugtracker is still down and will be fixed soon.

Slides and Lecture Notes of EJCP 2014 (2014-09-08)

The material of the course given at Ecole des Jeunes Chercheurs en Programmation (EJCP) in May 2014 is now available via the Documentation page. This document introduces the aims of proving software and shows application using FoCaLiZe.

Update of tutorial "Playing with proofs" (2014-03-06)

The tutorial "Playing with Proofs" available in the distribution and via the Documentation page has been updated to make the proof dealing with tree mirror working again. We still have to add few words to explain clearly how to state induction hypotheses in case of multiple recursive calls. Some words also have to be added about the shape of the goals and the equivalent shapes they can have to allow Zenon to use induction. Will be done ASAP ;)

Fixed broken links to papers in resources (2014-02-14)

Due to a site migration, some links to papers available in the Resources page got broken. The PDF files are now back.

final let-definitions available (2014-01-31)

A new feature is now available (currently only from the GIT repository) allowing to forbid redefinitions of let-definitions (logical or not): the final qualifier. This feature was requested to avoid duplicating the code of a logical let by adding a theorem paraphrasing the definition's body in order to prevent further redefinitions from changing the definition. For sake of homogeneity, "final-ity" is available also for "non-logical" definitions.

The following code*:
  logical let is_A_singleton = all a : A, A!equal (a, A!element);
  (* Theorem to avoid changes of is_A_singleton. *)
  theorem is_A_singleton_spec :
     is_A_singleton <-> all a : A, A!equal (a, A!element)
  proof = by definition of is_A_singleton ;


may now be simplified in:

  logical final let is_A_singleton = all a : A, A!equal (a, A!element);

Since no children in the inheritance will be allowed to alter the "meaning" of is_A_singleton, the theorem is_A_singleton_spec is no more needed.

(*) Thank's to Mathieu and Théo for the example.

Fix of the Zenon GIT repository (2014-01-17)

Zenon GIT repository got corrupted causing an incorrect git clone when used as anynymous user via the http link provided in the Download page. The version that was fetched did not include number of (more or less) recent commits, hence did not make available bug fixes and features of Zenon.

This is now fixed, users can clone or update their version of Zenon. Versions prior to 0.7.2 [a257] 2014-01-05 are out-of-date and were possibly impacted by the repository corruption.

Split of FoCaLiZe and Zenon GIT repositories (2013-04-08)

FoCaLiZe and Zenon are now in two separate GIT repositories. This won't impact the available material but now requires to clone both repositories. This split allows lighter installation when only needing Zenon. Until Zenon's repository is cleanly integrated as a sub-module of the FoCaLiZe one, these two separate clone/pull/push processes are required.

Bug tracking now available (2013-01-21)

Bugs, feature requests etc. can now be submitted via the FoCaLiZe bug tracker (powered by Bugzilla). We encourage this process instead of direct mails since it allows keeping trace of requests, prevents "memory loss" (the post-it stuck on the screen and finally falling down in the bin or whatever else) and can be used as knowledge database before submitting new requests.

Extended tutorial "Playing with Proofs" (2013-01-21)

The online version of the tutorial about proofs now contains a section dedicated to explicit induction, i.e. when Zenon does not succeed in finding a proof in a fully automatic way. This section shows how to apply the usual scheme of proof by induction, proving base cases, then induction cases under induction hypotheses.

New release (0.8.0) of the FoCaLiZe environment (2013-01-10)

The new release of the FoCaLiZe environment, focalize 0.8.0, is now available. FoCaLiZe got nearly asleep for some years, without major release despite some underground works. The "ghost" 0.7.0 version never became public, but the 0.8.0 cumulating the evolutions of the repository is nearly ready. Get the last version from the Download page and the related documentation from the Documentation page.
After a pretty long time without release, this new version brings number of enhancements, from the focalizec compiler and Zenon. New versions of OCaml and Coq are now supported as well as previous ones for sake of legacy. Zenon made impressive progress so as to be helpful in proving inductive properties for species. Installation and setup have been fully revisited, leading in a simpler and lighter mechanism. The standard library has been extended with low-level theorems. Termination proofs for structurally recursive functions are now possible. A certains number of bugs found in the focalizec compiler have been fixed. And a new tutorial about making proofs with Zenon is born. A complete description of changes / new features can in found in the CHANGES file of the distribution.

Initial event: The SSURF ANR project

The SSURF (Safety and Security UndeR Focal) ANR project was the starting point of the concretization of the FoCaLiZe environment, leading to an effective implementation of what is now the focalizec compiler, greatly helped by Zenon.
As a summary, this project consisted in :

Further information (in french) can be found here.


Last modification date: Tuesday, May 23rd, 2023 on host dhcpuei9.ensta.fr by user didou.
Copyright © 2005 - 2023 INRIA & LIP6, 2012 - 2023 ENSTA ParisTech, all rights reserved.