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).
Key | Value |
programName | sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c |
programSHA | 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9 |
witnessName | results-verified/symbiotic.2018-12-07_2142.logfiles/sv-comp19_prop-reachsafety.Problem06_label09_false-unreach-call.c.files/witness.graphml |
witnessSHA | 1f97f3f9282924965b8b2871939ac8b0304c6ab6206d1956a5cbb43c98147fb4 |
Key | Value |
architecture | 32bit |
creationtime | 2018-12-08T05:34 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_8ed6c291-ec5a-4411-9625-e6e3981e1a68/sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c |
programhash | 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/1f97f3f9282924965b8b2871939ac8b0304c6ab6206d1956a5cbb43c98147fb4.graphml |
witness-sha256 | 1f97f3f9282924965b8b2871939ac8b0304c6ab6206d1956a5cbb43c98147fb4 |
witness-size | 1261 |
witness-type | violation_witness |
This witness was created for this program (cf. table above, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9).
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 8 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
fb0be24 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 459 | 2019-12-04T00:31 CET (comp) | ||
8a8f067 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 1596 | 2019-12-11T21:43:31+01:00 | fbb35b6 | |
80cd2f9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 1596 | 2019-12-11T20:54:46+01:00 | da8ef66 | |
16f1f2e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 1596 | 2019-12-11T20:44:36+01:00 | 13df275 | |
71a7170 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 2131 | 2019-12-04T02:58:12+01:00 | fb0be24 | |
166c650 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 1595 | 2019-12-03T08:08:58+01:00 | 5ac6c9a | |
5ac6c9a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 1611 | 2019-11-30T09:26:41+01:00 | ||
fbb35b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 1618 | 2019-12-01T01:58:10+01:00 |
Found 12 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
1f97f3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T05:34 CET (sv-comp) | ||
2ab17dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 498 | 2018-12-07T10:40 CET (sv-comp) | ||
9bbfddc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 1611 | 2018-12-08T03:38:15+01:00 | ||
2f7e48b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1596 | 2018-12-09T18:21:22+01:00 | 5316811 | |
e795ee0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1613 | 2018-12-08T23:45:35+01:00 | 1f97f3f | |
742b2e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1595 | 2018-12-08T08:27:32+01:00 | 9bbfddc | |
ef8248b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1596 | 2018-12-08T05:05:59+01:00 | 9ee4536 | |
cdbcb94 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 2131 | 2018-12-07T17:45:07+01:00 | 2ab17dd | |
e29e4eb | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1596 | 2018-12-06T10:18:16+01:00 | 955f029 | |
bb3acd9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1596 | 2018-12-06T09:49:30+01:00 | fbdfafc | |
105ac75 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 2132 | 2018-12-06T09:14:25+01:00 | 8f47720 | |
fbdfafc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 1627 | 2018-12-05T12:18:20+01:00 |
Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
591b816 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T06:24 CET (sv-comp) | ||
6ce355d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 5 | 2017-12-01T17:32:01.641400 | ||
05828e3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 5 | 2017-12-01T19:41:54.796258 | ||
d944f8f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 890 | 2017-11-30T19:24:50+01:00 | ||
3c34b4d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 568 | 2017-11-30T19:40 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem06_label09_false-unreach-call.c, 404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/404516f8e1f79cc66fccb18bcaa9070fa42d60dbfd59c6173d71f335521f88e9.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |