Witness Inspection
A description of this web service can be found in the CAV paper
"Verification-Aided Debugging: An Interactive Web-Service for Exploring Error Witnesses"
(more material).
View and Validate the Witness
Input Given to this Service about the Witness (URL Query)
Key |
Value |
programName |
sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c |
programSHA |
77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44 |
witnessName |
results-verified/uautomizer.2017-12-02_0106.logfiles/sv-comp18.Ackermann01_true-unreach-call_true-no-overflow.c.files/witness.graphml |
witnessSHA |
063e896d54396c4dddd47c85354327086971844debf705539eedaa35510967db |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/063e896d54396c4dddd47c85354327086971844debf705539eedaa35510967db.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-02T21:24Z |
producer |
Automizer |
program-sha256 |
77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_c79f039d-fb8f-4e0d-8e90-0a0d4de007a7/sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c |
programhash |
c2f1e635c5c806286d01eb0b8ff07448b8253a7a |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
|
witness-file |
witnessFileByHash/063e896d54396c4dddd47c85354327086971844debf705539eedaa35510967db.graphml |
witness-sha256 |
063e896d54396c4dddd47c85354327086971844debf705539eedaa35510967db |
witness-size |
10821 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 7 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
382ab29 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
9 |
2019-11-30T23:30:48+01:00 |
|
ae98999 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
9 |
2019-12-11T20:13:05+01:00 |
860396f |
e03d8ae |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
9 |
2019-12-07T23:38:43+01:00 |
c5030ff |
57f7cbd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
9 |
2019-12-07T19:45:16+01:00 |
e7d4159 |
7abd190 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
9 |
2019-11-30T17:02:33+01:00 |
c48152c |
c48152c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
9 |
2019-11-30T04:10:31+01:00 |
|
860396f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
9 |
2019-11-30T23:44:57+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 12 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
71887cc |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T04:53:25 |
|
d4f0697 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
9 |
2018-12-08T03:05:12+01:00 |
|
62ffaa7 |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-06T07:30:44+01:00 |
|
e4f5cb1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
SMACK 1.9.3 |
3 |
2018-12-08T16:32:18 |
|
5d88a09 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn b8d6131600+ |
9 |
2018-12-07T03:17:25+01:00 |
|
47d39cc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-09T20:23:24+01:00 |
18a4568 |
a8c2d98 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-09T17:36:21+01:00 |
48db037 |
4e2a493 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-08T21:34:20+01:00 |
e4f5cb1 |
48001f4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-08T06:16:13+01:00 |
5d88a09 |
e46b448 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-06T09:28:35+01:00 |
4c098bd |
cac799d |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-06T09:00:21+01:00 |
95fed77 |
95fed77 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
9 |
2018-12-05T06:01:18+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 12 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
d0558cf |
Inspect |
|
CHECK( init(main()), LTL(G ! overflow) ) |
correctness_witness |
ESBMC 3.1 |
10 |
2017-12-01T14:30 CET (sv-comp) |
|
7d433ac |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
14 |
2017-11-30T20:54:02+01:00 |
|
25263f1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
6 |
2017-11-30T15:49:03+01:00 |
|
63ff83a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker (unknown version) |
8 |
2017-12-02T05:07:52+01:00 |
|
a73a4da |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
VIAP |
31 |
2017-12-03T04:00 CET (sv-comp) |
|
6327e82 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
10 |
2017-11-30T23:06 CET (sv-comp) |
|
42cd8bc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-03T04:24:23+01:00 |
148add6 |
ddab749 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-02T23:36:27+01:00 |
915fb53 |
dda201b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-01T08:13:16+01:00 |
6d83bc1 |
7ab52e7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-12-01T07:12:12+01:00 |
d15cba0 |
f0fa61e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.6.1-svn 26773 |
9 |
2017-11-30T13:31:30+01:00 |
|
063e896 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
Automizer |
11 |
2017-12-02T21:24Z |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44, sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c).
Found 0 witnesses for program sv-benchmarks/c/recursive/Ackermann01_true-unreach-call_true-no-overflow.c, 77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/77b30ed71d367a9eda341b05049d8050b9ab8f07e937028b34ed6cfd2c61cf44.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |