[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
Caduceus.

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

  http://www.frama-c.cea.fr/acsl.html

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