Docs GODI Archive
Projects Blog Link DB

Look up function:

(e.g. "List.find" or "keysym")
More options

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.14
Homepage: http://why.lri.fr
Maintainer: Virgile Prevosto <virgile.prevosto@m4x.org>
Files: bin/caduceus
bin/gwhy
bin/gwhy-bin
bin/jessie
bin/krakatoa
bin/rv_merge
bin/simplify2why
bin/why
bin/why-cpulimit
bin/why-dp
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_type_var.cmi
lib/jessie/jc_type_var.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/File.java
lib/krakatoa/java_api/java/io/FileDescriptor.java
lib/krakatoa/java_api/java/io/FileNotFoundException.java
lib/krakatoa/java_api/java/io/FileReader.java
lib/krakatoa/java_api/java/io/FilterOutputStream.java
lib/krakatoa/java_api/java/io/IOException.java
lib/krakatoa/java_api/java/io/InputStream.java
lib/krakatoa/java_api/java/io/InputStreamReader.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/Reader.java
lib/krakatoa/java_api/java/io/Serializable.java
lib/krakatoa/java_api/java/io/StreamTokenizer.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/Double.java
lib/krakatoa/java_api/java/lang/Exception.java
lib/krakatoa/java_api/java/lang/IllegalArgumentException.java
lib/krakatoa/java_api/java/lang/Integer.java
lib/krakatoa/java_api/java/lang/Long.java
lib/krakatoa/java_api/java/lang/Math.java
lib/krakatoa/java_api/java/lang/Number.java
lib/krakatoa/java_api/java/lang/NumberFormatException.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/HashMapIntegerInteger.java
lib/krakatoa/java_api/java/util/Iterator.java
lib/krakatoa/java_api/java/util/Locale.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.14
This web site is published by Informatikbüro Gerd Stolpmann
Powered by Caml