[Why-discuss] ACSL release 1.2
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.
More information about the Why-discuss