Using the CLI

Using AProVE from the Command Line

AProVE can be invoked as a standalone JAR from any terminal. After building with ant -f build-aprove.xml dist, the executable JAR is at dist/lib/aprove.jar.

Basic invocation

java -jar dist/lib/aprove.jar [OPTIONS] <input-file>

The input file is typically an .ari file (ARI format) or an .xml file (XTC/WST format). The goal, rewrite strategy, and start term are normally declared inside the .ari file itself.

Common options

Flag	Argument	Description
-t	<seconds>	Timeout in seconds (0 = no timeout)
-s	<strategy>	Strategy file or module name (e.g. aprove.strategies.Default)
-p	<format>	Proof output format: plain, html, tex, xml, cpf
-C	<certifier>	Certifier: ceta, cert, etc.
-m	<mode>	Run mode: aprove (default), wst, benchmark, quiet, cgi
-w	<n>	Number of parallel worker threads
-a	<mode>	Handling mode: termination, complexity, theoremprover

Overriding .ari file declarations

Three flags let you override declarations that are written inside the .ari file, without modifying the file. This is especially useful for batch runs or when testing a single file under different settings.

--goal / -G

Overrides the goal declared in the .ari file.

java -jar aprove.jar --goal ast   problem.ari
java -jar aprove.jar --goal sast  problem.ari
java -jar aprove.jar -G termination problem.ari

Accepted values (case-insensitive):

Value	Meaning
ast	Almost-sure termination (PTRS)
sast	Strong almost-sure termination (PTRS)
termination	Termination
complexity	Runtime complexity
confluence	Confluence
infeasibility	Infeasibility
past	Positive almost-sure termination (PTRS)

--rewrite-strategy / -R

Overrides the rewrite strategy declared in the .ari file.

java -jar aprove.jar --rewrite-strategy innermost problem.ari
java -jar aprove.jar -R full problem.ari

Accepted values: innermost, outermost, full

--startterm / -S

Overrides the start-term restriction declared in the .ari file.

java -jar aprove.jar --startterm basic problem.ari
java -jar aprove.jar -S all problem.ari

Accepted values: all, basic (matches the .ari grammar keywords ALL / BASIC)

Examples

Analyze a PTRS file for almost-sure termination with a 60-second timeout:

java -jar dist/lib/aprove.jar -t 60 --goal ast problem.ari

Override an innermost PTRS problem to run full rewriting:

java -jar dist/lib/aprove.jar --rewrite-strategy full problem.ari

Produce a CPF certificate alongside the result:

java -jar dist/lib/aprove.jar -p cpf -C ceta problem.ari

Notes

• --goal, --rewrite-strategy, and --startterm are applied after the .ari file is parsed but before the obligation is created, so they silently replace conflicting declarations in the file.
• Not all combinations of goal and rewrite strategy are meaningful for every language. AProVE will proceed with the override regardless; unexpected combinations typically result in MAYBE.
• For batch evaluation see Benchmarking.