•                                                                    *
  

• The Why platform for program certification *

•                                                                    *
  

• Copyright (C) 2002-2015 *

•                                                                    *
  

• Jean-Christophe FILLIATRE, CNRS & Univ. Paris-sud *
• Claude MARCHE, INRIA & Univ. Paris-sud *
• Yannick MOY, Univ. Paris-sud *
• Romain BARDOU, Univ. Paris-sud *

•                                                                    *
  

• Secondary contributors: *

•                                                                    *
  

• Thierry HUBERT, Univ. Paris-sud (former Caduceus front-end) *
• Nicolas ROUSSET, Univ. Paris-sud (on Jessie & Krakatoa) *
• Ali AYAD, CNRS & CEA Saclay (floating-point support) *
• Sylvie BOLDO, INRIA (floating-point support) *
• Jean-Francois COUCHOT, INRIA (sort encodings, hyps pruning) *
• Mehdi DOGGUY, Univ. Paris-sud (Why GUI) *

•                                                                    *
  

• Copyright (C) 2015-2019 *
• AstraVer fork: *
• Mikhail MANDRYKIN, ISP RAS (adaptation for Linux sources) *

•                                                                    *
  

• This software is free software; you can redistribute it and/or *
• modify it under the terms of the GNU Lesser General Public *
• License version 2.1, with the special exception on linking *
• described in file LICENSE. *

•                                                                    *
  

• This software is distributed in the hope that it will be useful, *
• but WITHOUT ANY WARRANTY; without even the implied warranty of *
• MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. *

•                                                                    *
  

AstraVer is a fork of the Jessie plug-in that allows deductive verification of C programs annotated with ACSL and is primarily targeted at Linux kernel modules source code. It uses the language and tools of the Why3 platform (http://why3.lri.fr/). Unlike original Jessie, AstraVer is not distributed as a part of the Why2 certification platform and is compiled/installed separately.

DOCUMENTATION

COPYRIGHT

This program is distributed under the GNU GPL. See the enclosed file COPYING.

INSTALLATION

See the enclosed file INSTALL.