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.

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.

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 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: Monday, April 8, 2013 on host macapuces by user Didou.
Copyright © 2005 - 2013 INRIA & LIP6, 2012 - 2013 ENSTA ParisTech, all rights reserved.