Be notified of new releases
Create your free GitHub account today to subscribe to this repository for new releases and build software alongside 28 million developers.Sign up
AProVE has several built-in summaries (e.g., for native methods and some standard library methods). Some of these built-in summaries are not always applicable (e.g., there's a summary for
String.equals for the case that both strings are known). So far, AProVE didn't generate a default summary if there was an inapplicable built-in summary. This new version first looks for a built-in (or user-provided) summary and checks if it's applicable. If this is not the case, then it generates a default summary (if the corresponding flags are enabled).
In rare cases, functional interfaces may have several abstract methods, see https://stackoverflow.com/questions/23721759/functionalinterface-comparator-has-2-abstract-methods. This is now supported by AProVE.
Supports the new option
-O java::analysis_goal=UserDefined where default summaries and all opcodes have cost 0. Thus, costs are only caused by user-provided summaries. This enables user-defined cost models like "only writing to files causes costs".
First version of AProVE that is able to treat integer variables of C programs as bitvectors or unbounded integers depending on the command-line option "-b". If set, the termination proof is started using bitvector semantics.
Experimental Java 8 support for AProVE. One important feature is still missing: The methods created by InvokeDynamic at runtime do not yet take care of implicit conversions. If they have to, AProVE hopefully crashes...
Pre-compiled KoAT binary for Windows. It neither supports apron nor z3's ocaml-bindings. Hence, it is significantly weaker and slower than the Linux version.
Version from the termination and complexity competition 2017 (except for the category
Integer Transition Systems certified, where AProVE '17 was used).
AProVE version similar to the version that was used for the termination and complexity competition 2017, but with the standard strategy (instead of the specialized competition strategy).
Moreover, in contrast to the competition version, this version has one additional fix to avoid rejects in the category
Integer Transition Systems certified. This fix is not needed for correctness, but just for certification. At the competition, it was only used for the category
Integer Transition Systems certified, since we did not have enough time to re-test all categories.
If you use AProVE from the command line, these are the most important command line flags:
-t $TIMEOUTto specify a timeout in seconds; This is especially important for complexity analysis, since AProVE sometimes tries to improve its results for a very long time.
-m wstto get the result of the analysis as first line on
-p plain|htmlto get a proof as plain text or html
Another convenient way to use AProVE is our Eclipse plugin which is available from our Eclipse update site.
For further information on command line options, AProVE's dependencies, and our Eclipse plugin, please visit our download site.
starexec_bundle.zip is built upon the same AProVE version, but uses the competition strategy. It is ready to run on starexec and contains the following configurations:
C Integer Programs
Complexity - C Integer Programs
Integer Transition Systems
Integer Transition Systems certified
certifiedfor all other certified categories
standardfor everything else
If you want to benchmark with AProVE, please use the preconfigured
starexec_bundle.zip if possible, since setting up AProVE with all its dependencies is tricky. Please note that
starexec_bundle.zip is optimized for a timeout of 300 seconds.
If you want to benchmark with AProVE, but
- cannot use
- want to use a different timeout, or
- experience any problems,
please write an e-mail to firstname.lastname@example.org.