AProVE '17

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 $TIMEOUT to 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 wst to get the result of the analysis as first line on stdout
• -p plain|html to 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.

The 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 for C and C Integer Programs
• c_complexity for Complexity - C Integer Programs
• inttrs for Integer Transition Systems
• inttrs_certified for Integer Transition Systems certified
• certified for all other certified categories
• standard for 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 starexec_bundle.zip,
• want to use a different timeout, or
• experience any problems,

please write an e-mail to aprove@i2.informatik.rwth-aachen.de.