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/systemc/pipeline_false-unreach-call_false-termination.cil.c |
programSHA |
792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33 |
witnessName |
results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.pipeline_false-unreach-call_false-termination.cil.c.files/witness.graphml |
witnessSHA |
a4ccc32c0ae806491f74b434abac193bd0a506db4c392081b7acb84d08726c9f |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/a4ccc32c0ae806491f74b434abac193bd0a506db4c392081b7acb84d08726c9f.json
Key |
Value |
architecture |
32bit |
creationtime |
2017-12-02T06:51 CET (sv-comp) |
producer |
Symbiotic |
program-sha256 |
792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33 |
programfile |
/tmp/vcloud-vcloud-master/worker/working_dir_277f8510-e62b-4ac5-a3e3-b52f27abb25a/sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c |
programhash |
757b17cdc808fcc00ce6a7984efa373572d69f7f |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file |
witnessFileByHash/a4ccc32c0ae806491f74b434abac193bd0a506db4c392081b7acb84d08726c9f.graphml |
witness-sha256 |
a4ccc32c0ae806491f74b434abac193bd0a506db4c392081b7acb84d08726c9f |
witness-size |
797 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.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 (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.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 (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.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 (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.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 (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 6 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
e05a041 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
674 |
2019-12-11T22:00:25+01:00 |
841b550 |
ba9fb0c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
761 |
2019-12-11T20:55:04+01:00 |
12091a1 |
b78aae6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
732 |
2019-12-11T20:44:49+01:00 |
b6ed986 |
841b550 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco |
663 |
2019-12-01T09:38:07+01:00 |
|
f1c7f1f |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
66 |
2019-12-05T20:21:00+01:00 |
f08d943 |
abe1fb7 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / svcomp20 |
4405 |
2019-11-30T09:57:00+01:00 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 11 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
efd3655 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-08T09:41 CET (sv-comp) |
|
8e070ed |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
SMACK 1.9.3 |
110 |
2018-12-08T12:55:48 |
|
23362a0 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
671 |
2018-12-07T15:40:08+01:00 |
|
f103ee3 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
741 |
2018-12-09T18:21:20+01:00 |
a2c6185 |
36670ff |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
702 |
2018-12-08T23:44:55+01:00 |
efd3655 |
e0b86c5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
685 |
2018-12-08T22:10:50+01:00 |
8e070ed |
2737644 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
674 |
2018-12-08T08:36:00+01:00 |
23362a0 |
95e0a03 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
758 |
2018-12-08T04:50:51+01:00 |
ce0ea14 |
83993c9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
758 |
2018-12-06T10:13:32+01:00 |
5d5008f |
bbea030 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
768 |
2018-12-06T09:19:47+01:00 |
b3ae736 |
74c3659 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
66 |
2018-12-10T20:37:22+01:00 |
fa23605 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 11 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
f839484 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
456 |
Sat Dec 2 18:10:22 2017 |
|
a4ccc32 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T06:51 CET (sv-comp) |
|
aa925e9 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
31 |
2017-12-01T13:12:05.372329 |
|
ae33174 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
29 |
2017-12-01T11:42:41.112981 |
|
58a33e5 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
138 |
2017-12-01T18:44 CET (sv-comp) |
|
5eeabe6 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
138 |
2017-12-01T04:11 CET (sv-comp) |
|
bfcd106 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
638 |
2017-11-30T22:24:27+01:00 |
|
bb05d9c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
479 |
2017-11-30T23:18:33+01:00 |
|
f8cb860 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
512 |
2017-12-01T01:54:32+01:00 |
|
54a9f00 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
467 |
2017-11-30T22:59 CET (sv-comp) |
|
0c71982 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
139 |
2017-12-01T15:46 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33, sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c).
Found 0 witnesses for program sv-benchmarks/c/systemc/pipeline_false-unreach-call_false-termination.cil.c, 792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/792a92719a4a915543c3a695278c547c03e5436ecf26c32914ca5da80f344b33.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |