Verification tasks are grouped in directories depending on their source,
e.g., jbmc-regression
.
Within these directories, each verification task consists of a YAML file
in the format defined by BenchExec for task-definition files.
These YAML files define the list of input files (Java sources) of a task
and the expected verdict for each possible property.
The programs are assumed to be written in Java 1.8.
All Java source files of a task need to have the suffix .java
.
Program files must have a copyright header indicating
the source of the benchmark (at least in the "main" source file).
The program may call the Java standard library (java.*
, javax.*
).
For each program at least one property file needs to be listed in the task-definition file, which defines the entry point and the property that the verifier should check.
For checking (un)reachability,
we use the assert
keyword provided in the Java language:
The property G assert
specifies that all assert
statements
in the program can never fail.
A property file that defines the method main
in the class Main
in the default package as the entry point,
and uses the assert property would look as follows:
CHECK( init(Main.main()), LTL(G assert) )
Other properties are currently not defined.
The verification task need to be compilable by putting all .java
files
in directories listed as input files on the sourcepath of a Java 8 compiler.
BenchExec will pass the paths
that are listed as input files in a task-definition file
to the tool-info module,
which can pass them to the verifier
or for example expand them to a list of single .java
files,
depending on what the verifier needs.
If a verification tool requires .class
files or a .jar
file as input
it should use regular Java utilities to create these artifacts
(in a wrapper script if necessary).
The only admissible source of nondeterminism are the return values of
the methods defined in the org.sosy_lab.sv_benchmarks.Verifier
class, provided in
java/common/org/sosy_lab/sv_benchmarks/Verifier.java
in the
sv-benchmarks
repository. In order to make the benchmarks
compilable, ../common/
needs to be added to the input_files
property of the benchmark's YAML file.
The methods in org.sosy_lab.sv_benchmarks.Verifier
call methods
of the java.util.Random
class. The rationale is to provide
straightforward compatibility with verifiers that implement a
nondeterministic semantics for the java.util.Random
class, i.e.
the methods in java.util.Random
are expected to return a
nondeterministic value instead of a random value, but satisfying
the same constraints on their value range.
org.sosy_lab.sv_benchmarks.Verifier
also provides an assume
method, which is defined as Runtime.getRuntime().halt(1)
. It is
recommended to use assume
or return
(if in the entry point method)
to restrict the nondeterminism as they do not impact the termination
behavior of a program. For example, using `while(!condition); would
make any program with such assumptions be classified non-terminating
when a potential Java Termination category might be introduced in
future.
Any library methods that make system calls are not allowed in verification tasks.