[Why-discuss] ACSL release 1.2

Jean-Christophe Filliâtre Jean-Christophe.Filliatre at lri.fr
Wed Mar 5 09:46:09 CET 2008

Dear list members,

The developers of the Why platform are currently collaborating with the
CEA to design and implement a common framework for the verification of C
programs, called Frama-C, which will eventually become the successor of

The first outcome of this collaboration is the design of a specification
language called ACSL, for "ANSI/ISO C Specification Language". This
language is greatly inspired by Caduceus specification language (itself
greatly inspired by JML). A first public version of ACSL is available at


Comments are welcome (and can be sent to this list).

A first release of Frama-C is expected by the end of the week; see the
web site above for more details about Frama-C.

Jean-Christophe Filliâtre

More information about the Why-discuss mailing list