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/termination-crafted/Mysore_false-termination_true-valid-memsafety.c |
programSHA |
6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34 |
witnessName |
results-verified/depthk.2017-12-01_1515.logfiles/sv-comp18.Mysore_false-termination_true-valid-memsafety.c.files/witness.graphml |
witnessSHA |
6838f0e5d3f80737efc9fc50fd4b1826c5bcca81caccff93f79fe56e9a176d21 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/6838f0e5d3f80737efc9fc50fd4b1826c5bcca81caccff93f79fe56e9a176d21.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-01T17:17 CET (sv-comp) |
memoryModel |
precise |
producer |
ESBMC 3.1 |
program-sha256 |
6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_c96fff84-94f7-42b6-853d-13f0623450ee/sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c |
programhash |
a7efd1a0f3e3646ffbf8e76b3eb61ab823f0d031 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/6838f0e5d3f80737efc9fc50fd4b1826c5bcca81caccff93f79fe56e9a176d21.graphml |
witness-sha256 |
6838f0e5d3f80737efc9fc50fd4b1826c5bcca81caccff93f79fe56e9a176d21 |
witness-size |
5766 |
witness-type |
correctness_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 4 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
0f74496 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.3 |
6 |
2023-11-30T08:22:50+01:00 |
|
c6d8ca8 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.2.1-svn-e677b7cd46+ |
6 |
2023-12-03T21:35:25+01:00 |
|
64930fd |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
6 |
2023-12-17T05:11:01+01:00 |
|
cebfe41 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2023-12-19T01:04:37+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '23
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 5 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
4c882bc |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.2 |
6 |
2022-12-10T15:47:58+01:00 |
|
a773f58 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.2.1-svn-1715bd67dc+ |
6 |
2022-12-11T23:44:46+01:00 |
|
4df843e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
6 |
2022-12-25T10:03:44+01:00 |
|
0a736e2 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-a45b42da2f+ |
6 |
2022-12-10T00:06:47+01:00 |
|
6bcb44d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
correctness_witness |
Bubaak |
3 |
2022-12-08T19:41:48Z |
|
Available Results for the Program from Witness Store SV-COMP '22
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 5 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
5d5b91e |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.1 |
6 |
2021-12-05T19:23:10+01:00 |
|
97a5a7d |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0 |
6 |
2021-12-10T17:19:39+01:00 |
|
c196736 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-fe6f522dd3+ |
6 |
2021-12-08T18:34:04+01:00 |
|
a8fc9fd |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2021-12-09T11:12:29+01:00 |
|
ed6f4c4 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
6 |
2021-12-06T17:05:02Z |
|
Available Results for the Program from Witness Store SV-COMP '21
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e4d9391 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0 |
6 |
2020-12-05T14:58:30+01:00 |
|
631f456 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
CPAchecker 2.0.1-svn-eda176372c+ |
6 |
2020-12-08T00:52:21+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '20
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 2 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6ef7dce |
Inspect |
|
CHECK( init(main()), LTL(G valid-memtrack) ) |
correctness_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ |
6 |
2019-12-01T02:05:44+01:00 |
|
6dab5b5 |
Inspect |
|
CHECK( init(main()), LTL(G valid-free) ) |
correctness_witness |
CPAchecker 1.9 |
6 |
2019-11-29T16:16:13+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.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 '18
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 1 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
6838f0e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
ESBMC 3.1 |
6 |
2017-12-01T17:17 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34, sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c).
Found 0 witnesses for program sv-benchmarks/c/termination-crafted/Mysore_false-termination_true-valid-memsafety.c, 6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6edfc33d3e5e116b8b5f39fddb65c59ef052d6dfaffe394b38d04501128bfe34.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |