Commit 4dc4876f authored by Dirk Beyer's avatar Dirk Beyer

Some rewording of the documentation text

parent d424b37c
# MetaVal - a Meta-Validator for Verification Witnesses
# MetaVal: A Meta-Validator for Verification Witnesses
MetaVal takes as input a program and a witness and reduces the task of validating the witness into a verification task.
For the transformation, CPAchecker is used as a frontend.
MetaVal takes as input a program, a specification, and a witness, and reduces the task of witness-based result validation to an ordinary verification task.
For the reduction, CPAchecker is used as program transformer.
At the backend, an arbitrary verifier can be used as long as it understands the specification format of SV-COMP.
As verification backend, any standard verifier can be used as long as it understands the specification format of SV-COMP.
## Execute using BenchExec
MetaVal is most conveniently called via BenchExec.
In your benchmark definition, all you have to do is to specify the following options:
The benchmark definition needs to specify the following options:
--metavalVerifierBackend
--metavalWitness
these are then filtered by benchexec's tool-info module and not actually passed to metaval.sh
These are then filtered by BenchExec's tool-info module and not actually passed to metaval.sh.
Example snippet from the SV-COMP task definition:
<option name="--metavalWitness">../../results-verified/LOGDIR/${rundefinition_name}.${taskdef_name}/witness.graphml</option>
<option name="--metavalVerifierBackend">cpachecker</option>
The currently supported backends are:
The currently supported verification backends are:
- cpachecker-metaval: use the CPAchecker version that is also used in the frontend
- cpachecker: use the CPAchecker version from the submission CPA-Seq of SV-COMP'2019
- symbiotic: use the Symbiotic version from the submission of SV-COMP'2019
- yogar-cbmc: use the Yogar-CBMC version from the submission of SV-COMP'2019
- ultimateautomizer: use the Ultimate Automizer version from the submission of SV-COMP'2019
- cpachecker-metaval: use the CPAchecker version that is also used as program transformer
- cpachecker: use the CPAchecker version from the submission CPA-Seq to SV-COMP'2019
- symbiotic: use the Symbiotic version from the submission to SV-COMP'2019
- yogar-cbmc: use the Yogar-CBMC version from the submission to SV-COMP'2019
- ultimateautomizer: use the Ultimate version from the submission UAutomizer to SV-COMP'2019
## Execute metaval.sh directly
If you want to call metaval directly, you can do so with the following syntax:
To call MetaVal directly, the following syntax can be used:
metaval.sh --witness path/to/witness --verifier nameOfVerifier -- $BACKENDVERIFIERCMD
$BACKENDVERIFIERCMD is the command with which you would normally call the backend verifier, assuming that you are in its directory.
You will also have to use ../output/ARG.c instead of the path to the original program from the task, since metaval will create the reduced program there.
$BACKENDVERIFIERCMD is the command with which the backend verifier would normally be called, assuming its directory as working directory.
The file ../output/ARG.c has to be used instead of the original program from the verification task, since MetaVal will create the reduced program there.
Example for using CPAchecker as verifier backend:
Example for using CPAchecker as verification backend:
./metaval.sh --verifier 'CPAchecker-1.7-svn 29852-unix' --witness witness.graphml \
../sv-benchmarks/c/bitvector/jain_1-1.c -- scripts/cpa.sh -predicateAnalysis-PredAbsRefiner-ABEl \
......
......@@ -25,7 +25,7 @@ shift
if [ "$1" != "--witness" ]
then
echo "expected a witness as seconf option, but got $1"
echo "expected a witness as second option, but got $1"
exit 1
fi
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment