************************************************************************** * * * The Why/Caduceus/Krakatoa tool suite for program certification * * Copyright (C) 2002-2006 * * Jean-François COUCHOT * * Mehdi DOGGUY * * Jean-Christophe FILLIÂTRE * * Thierry HUBERT * * Claude MARCHÉ * * Yannick MOY * * * * This software is free software; you can redistribute it and/or * * modify it under the terms of the GNU General Public * * License version 2, as published by the Free Software Foundation. * * * * 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. * * * * See the GNU General Public License version 2 for more details * * (enclosed in the file GPL). * * * ************************************************************************** Why is a certification tool. It takes annotated programs as input and outputs proof obligations for the proof assistants PVS and Coq. DOCUMENTATION ============= The documentation (a tutorial and a reference manual) is enclosed in the subdirectory doc/. Various examples can be found in the subdirectory examples/. Mailing lists: there exist two mailing lists for Why and Caduceus respectively. To subscribe, you need to send an email to why-request@serveur-listes.lri.fr or caduceus-request@serveur-listes.lri.fr with "subscribe your@email" in the mail body. These lists are mainly used to announce the releases of Why and Caduceus. Emails can be sent to the list at why@serveur-listes.lri.fr and caduceus@serveur-listes.lri.fr. Only the lists members can send emails to the list. COPYRIGHT ========= This program is distributed under the GNU GPL. See the enclosed file COPYING. INSTALLATION ============ See the enclosed file INSTALL.