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/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c |
programSHA |
3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121 |
witnessName |
results-verified/2ls.2018-12-04_2244.logfiles/sv-comp19_prop-termination.Problem14_label12_false-unreach-call_false-termination.c.files/witness.graphml |
witnessSHA |
21ede9251b0515148f7dd6e569bd2a200820a61b8728cb728038eb38d97c3614 |
Information about the Witness from Competition Database
from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/21ede9251b0515148f7dd6e569bd2a200820a61b8728cb728038eb38d97c3614.json
Key |
Value |
architecture |
32bit |
creationtime |
2018-12-05T09:32 CET (sv-comp) |
producer |
2LS |
programfile |
../../sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c |
programhash |
21e636d8dc14d5889feae0d6b5b1b339be6780f9 |
sourcecodelang |
C |
specification |
CHECK( init(main()), LTL(F end) ) |
witness-file |
witnessFileByHash/21ede9251b0515148f7dd6e569bd2a200820a61b8728cb728038eb38d97c3614.graphml |
witness-sha256 |
21ede9251b0515148f7dd6e569bd2a200820a61b8728cb728038eb38d97c3614 |
witness-size |
582662 |
witness-type |
violation_witness |
Available Results for the Program from Witness Store SV-COMP '24
Trying to find witnesses for program (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.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 (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.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 (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.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 (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.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 (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 11 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
52f70ee |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
4 |
2019-12-02 03:44:30 |
|
e74f817 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
414 |
2019-12-04T00:21 CET (comp) |
|
3b1fafb |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1340 |
2019-12-11T21:09:37+01:00 |
52f70ee |
923f8a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1453 |
2019-12-11T20:44:38+01:00 |
09e3d8d |
0c7bacd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1674 |
2019-12-04T02:58:28+01:00 |
e74f817 |
1ef9bda |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / witnessValidation |
1340 |
2019-12-03T08:10:46+01:00 |
6677ec4 |
6677ec4 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.9 / svcomp20 |
1339 |
2019-11-30T04:12:24+01:00 |
|
8c0ce24 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-11T20:54:49+01:00 |
3f944c0 |
7af2e82 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-07T21:18:26+01:00 |
ebabec4 |
c67f96e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.9 / witnessValidation |
301 |
2019-12-05T20:22:27+01:00 |
1f0889b |
f659106 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Symbiotic |
4 |
2019-12-02 02:08:11 |
|
Available Results for the Program from Witness Store SV-COMP '19
Trying to find witnesses for program (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 13 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
498aaaa |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2018-12-07T23:05 CET (sv-comp) |
|
1478c8b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Pinaka |
485 |
2018-12-07T09:58 CET (sv-comp) |
|
e8afbfd |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn b8d6131600+ |
1345 |
2018-12-08T04:21:01+01:00 |
|
3d83d32 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1340 |
2018-12-09T17:49:07+01:00 |
26c9c8f |
4b107cc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1340 |
2018-12-08T08:00:39+01:00 |
e8afbfd |
93210c2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1674 |
2018-12-07T17:11:30+01:00 |
1478c8b |
822f39b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1340 |
2018-12-06T09:48:03+01:00 |
7cb69d1 |
93a1915 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1890 |
2018-12-06T09:07:14+01:00 |
13cbe89 |
7cb69d1 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.7-svn 29852 |
1339 |
2018-12-05T14:35:20+01:00 |
|
4a19c41 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:53:51+01:00 |
453388a |
dede5ac |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-09T20:40:05+01:00 |
5f4ac3e |
aa5f00b |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T23:45:04+01:00 |
498aaaa |
dcef3df |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
correctness_witness |
CPAchecker 1.7-svn 29852 |
301 |
2018-12-08T05:01:08+01:00 |
77b9448 |
Available Results for the Program from Witness Store SV-COMP '18
Trying to find witnesses for program (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |
b6f1a84 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
VeriAbs 1.3 |
801 |
Sat Dec 2 19:40:40 2017 |
|
9e3b334 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Symbiotic |
1 |
2017-12-02T00:43 CET (sv-comp) |
|
73539fc |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 kind |
8 |
2017-12-01T23:47:02.421609 |
|
13b33a2 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 4.6.0 incr |
9 |
2017-12-01T14:57:16.348221 |
|
7345a99 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
ESBMC 3.1 |
23 |
2017-12-01T16:38 CET (sv-comp) |
|
154a92c |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26773 |
721 |
2017-11-30T13:06:10+01:00 |
|
ad86152 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26758M |
978 |
2017-12-01T03:08:06+01:00 |
|
f8ed92e |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CPAchecker 1.6.1-svn 26725 |
719 |
2017-11-30T23:55:41+01:00 |
|
25d978a |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
CBMC |
606 |
2017-11-30T22:03 CET (sv-comp) |
|
4b99157 |
Inspect |
|
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
violation_witness |
Automizer |
1024 |
2017-12-02T04:28Z |
|
5b52932 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
Automizer |
147 |
2017-12-03T11:15Z |
|
f184ef3 |
Inspect |
|
CHECK( init(main()), LTL(F end) ) |
violation_witness |
2LS |
577 |
2017-12-01T12:45 CET (sv-comp) |
|
Available Results for the Program from Witness Store SV-COMP '17
Trying to find witnesses for program (3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121, sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem14_label12_false-unreach-call_false-termination.c, 3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/3a67fb41e69fd0e39587aad4fc36732dd58ffb2b7984addc47642617e072f121.json
Show Witness |
Inspect |
Validate |
Specification |
Result Type |
Producer |
Size (kB) |
Time stamp |
Input Witness |