FREE SOFTWARE ON CAMLCITY.ORG

GODI Package apps-why

Verification condition generator for various systems

Why is a software verification tool. Why aims at being a verification conditions generator (VCG) back-end for other verification tools. It provides a powerful input language including higher-order functions, polymorphism, references, arrays and exceptions. It generates proof obligation for proof assistants and automated theorem provers. Some of them (namely Coq and zenon) are available as Godi packages as well. Other ones have to be installed by hand. You need at least one system installed for Why to be useful. The front-end for Why currently includes Krakatoa (for Java programs) and Caduceus (for C programs). Caduceus is included in the Why distribution itself.

Version:	2.13godi1
Homepage:	"http://why.lri.fr"
Maintainer:	"Virgile Prevosto <virgile.prevosto@m4x.org>"
Files:	bin/caduceus bin/cpulimit bin/dp bin/gwhy bin/gwhy-bin bin/jessie bin/krakatoa bin/rv_merge bin/simplify2why bin/why bin/why-obfuscator bin/why-stat bin/why2html lib/caduceus/coq/caduceus_tactics.v lib/caduceus/coq/caduceus_why.v lib/caduceus/harvey/caduceus_why.rv lib/caduceus/isabelle/caduceus_why.thy lib/caduceus/why/caduceus.why lib/caduceus/why/caduceus_arith.why lib/coq/user-contrib/Caduceus.v lib/coq/user-contrib/Caduceus.vo lib/coq/user-contrib/Why.v lib/coq/user-contrib/Why.vo lib/coq/user-contrib/WhyArrays.v lib/coq/user-contrib/WhyArrays.vo lib/coq/user-contrib/WhyBool.v lib/coq/user-contrib/WhyBool.vo lib/coq/user-contrib/WhyCM.v lib/coq/user-contrib/WhyCM.vo lib/coq/user-contrib/WhyCoqCompat.v lib/coq/user-contrib/WhyCoqCompat.vo lib/coq/user-contrib/WhyExn.v lib/coq/user-contrib/WhyExn.vo lib/coq/user-contrib/WhyInt.v lib/coq/user-contrib/WhyInt.vo lib/coq/user-contrib/WhyLemmas.v lib/coq/user-contrib/WhyLemmas.vo lib/coq/user-contrib/WhyPermut.v lib/coq/user-contrib/WhyPermut.vo lib/coq/user-contrib/WhyPrelude.v lib/coq/user-contrib/WhyPrelude.vo lib/coq/user-contrib/WhyReal.v lib/coq/user-contrib/WhyReal.vo lib/coq/user-contrib/WhySorted.v lib/coq/user-contrib/WhySorted.vo lib/coq/user-contrib/WhyTactics.v lib/coq/user-contrib/WhyTactics.vo lib/coq/user-contrib/WhyTuples.v lib/coq/user-contrib/WhyTuples.vo lib/coq/user-contrib/caduceus_lists.v lib/coq/user-contrib/caduceus_lists.vo lib/coq/user-contrib/caduceus_tactics.v lib/coq/user-contrib/caduceus_tactics.vo lib/coq/user-contrib/caduceus_why.v lib/coq/user-contrib/caduceus_why.vo lib/coq/user-contrib/jessie_why.v lib/coq/user-contrib/jessie_why.vo lib/jessie/coq/jessie_why.v lib/jessie/jc.cmi lib/jessie/jc.cmi_pretty lib/jessie/jc.cmo lib/jessie/jc.cmx lib/jessie/jc.o lib/jessie/jc_ast.cmi lib/jessie/jc_ast.cmi_pretty lib/jessie/jc_common_options.cmi lib/jessie/jc_common_options.cmi_pretty lib/jessie/jc_constructors.cmi lib/jessie/jc_constructors.cmi_pretty lib/jessie/jc_env.cmi lib/jessie/jc_env.cmi_pretty lib/jessie/jc_envset.cmi lib/jessie/jc_envset.cmi_pretty lib/jessie/jc_fenv.cmi lib/jessie/jc_fenv.cmi_pretty lib/jessie/jc_iterators.cmi lib/jessie/jc_iterators.cmi_pretty lib/jessie/jc_noutput.cmi lib/jessie/jc_noutput.cmi_pretty lib/jessie/jc_output.cmi lib/jessie/jc_output.cmi_pretty lib/jessie/jc_output_misc.cmi lib/jessie/jc_output_misc.cmi_pretty lib/jessie/jc_pervasives.cmi lib/jessie/jc_pervasives.cmi_pretty lib/jessie/jc_poutput.cmi lib/jessie/jc_poutput.cmi_pretty lib/jessie/jc_region.cmi lib/jessie/jc_region.cmi_pretty lib/jessie/jc_version.cmi lib/jessie/jc_version.cmi_pretty lib/jessie/lib.cmi lib/jessie/lib.cmi_pretty lib/jessie/loc.cmi lib/jessie/loc.cmi_pretty lib/jessie/option_misc.cmi lib/jessie/option_misc.cmi_pretty lib/jessie/output.cmi lib/jessie/output.cmi_pretty lib/jessie/pp.cmi lib/jessie/pp.cmi_pretty lib/jessie/rc.cmi lib/jessie/rc.cmi_pretty lib/jessie/why/jessie.why lib/krakatoa/java_api/java/io/BufferedWriter.java lib/krakatoa/java_api/java/io/FilterOutputStream.java lib/krakatoa/java_api/java/io/ObjectStreamClass.java lib/krakatoa/java_api/java/io/OutputStream.java lib/krakatoa/java_api/java/io/OutputStreamWriter.java lib/krakatoa/java_api/java/io/PrintStream.java lib/krakatoa/java_api/java/io/Serializable.java lib/krakatoa/java_api/java/lang/ArrayStoreException.java lib/krakatoa/java_api/java/lang/CharSequence.java lib/krakatoa/java_api/java/lang/Class.java lib/krakatoa/java_api/java/lang/Cloneable.java lib/krakatoa/java_api/java/lang/Comparable.java lib/krakatoa/java_api/java/lang/Exception.java lib/krakatoa/java_api/java/lang/Integer.java lib/krakatoa/java_api/java/lang/Math.java lib/krakatoa/java_api/java/lang/Number.java lib/krakatoa/java_api/java/lang/Object.java lib/krakatoa/java_api/java/lang/RuntimeException.java lib/krakatoa/java_api/java/lang/String.java lib/krakatoa/java_api/java/lang/StringBuffer.java lib/krakatoa/java_api/java/lang/System.java lib/krakatoa/java_api/java/lang/Throwable.java lib/krakatoa/java_api/java/util/AbstractMap.java lib/krakatoa/java_api/java/util/Collection.java lib/krakatoa/java_api/java/util/HashMap.java lib/krakatoa/java_api/java/util/Iterator.java lib/krakatoa/java_api/java/util/Map.java lib/krakatoa/java_api/java/util/Set.java lib/krakatoa/javacard_api/com/sun/javacard/impl/Constants.java lib/krakatoa/javacard_api/com/sun/javacard/impl/NativeMethods.java lib/krakatoa/javacard_api/com/sun/javacard/impl/PackedBoolean.java lib/krakatoa/javacard_api/com/sun/javacard/impl/PrivAccess.java lib/krakatoa/javacard_api/java/lang/ArrayIndexOutOfBoundsException.java lib/krakatoa/javacard_api/java/lang/Exception.java lib/krakatoa/javacard_api/java/lang/IndexOutOfBoundsException.java lib/krakatoa/javacard_api/java/lang/Object.java lib/krakatoa/javacard_api/java/lang/RuntimeException.java lib/krakatoa/javacard_api/java/lang/Throwable.java lib/krakatoa/javacard_api/javacard/framework/AID.java lib/krakatoa/javacard_api/javacard/framework/APDU.java lib/krakatoa/javacard_api/javacard/framework/APDUException.java lib/krakatoa/javacard_api/javacard/framework/Applet.java lib/krakatoa/javacard_api/javacard/framework/CardException.java lib/krakatoa/javacard_api/javacard/framework/CardRuntimeException.java lib/krakatoa/javacard_api/javacard/framework/Dispatcher.java lib/krakatoa/javacard_api/javacard/framework/ISO7816.java lib/krakatoa/javacard_api/javacard/framework/ISOException.java lib/krakatoa/javacard_api/javacard/framework/JCSystem.java lib/krakatoa/javacard_api/javacard/framework/OwnerPIN.java lib/krakatoa/javacard_api/javacard/framework/PIN.java lib/krakatoa/javacard_api/javacard/framework/PINException.java lib/krakatoa/javacard_api/javacard/framework/Shareable.java lib/krakatoa/javacard_api/javacard/framework/SystemException.java lib/krakatoa/javacard_api/javacard/framework/TransactionException.java lib/krakatoa/javacard_api/javacard/framework/UserException.java lib/krakatoa/javacard_api/javacard/framework/Util.java lib/krakatoa/javacard_api/javacard/security/CryptoException.java lib/krakatoa/javacard_api/javacard/security/DESKey.java lib/krakatoa/javacard_api/javacard/security/DSAKey.java lib/krakatoa/javacard_api/javacard/security/DSAPrivateKey.java lib/krakatoa/javacard_api/javacard/security/DSAPublicKey.java lib/krakatoa/javacard_api/javacard/security/Key.java lib/krakatoa/javacard_api/javacard/security/KeyBuilder.java lib/krakatoa/javacard_api/javacard/security/KeyPair.java lib/krakatoa/javacard_api/javacard/security/MessageDigest.java lib/krakatoa/javacard_api/javacard/security/PrivateKey.java lib/krakatoa/javacard_api/javacard/security/PublicKey.java lib/krakatoa/javacard_api/javacard/security/RSAPrivateCrtKey.java lib/krakatoa/javacard_api/javacard/security/RSAPrivateKey.java lib/krakatoa/javacard_api/javacard/security/RSAPublicKey.java lib/krakatoa/javacard_api/javacard/security/RandomData.java lib/krakatoa/javacard_api/javacard/security/SecretKey.java lib/krakatoa/javacard_api/javacard/security/Signature.java lib/krakatoa/javacard_api/javacardx/crypto/Cipher.java lib/why/arrays.why lib/why/floats.why lib/why/mix.why lib/why/prelude.why lib/why/why-logo-1.png share/man/man1/why.1.html
Built from sources:	why-2.13

This web site is published by Informatikbüro Gerd Stolpmann


Docs	GODI	Archive
Projects	Blog	Link DB