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/Problem03_label26_false-unreach-call.c |
programSHA | 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08 |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.Problem03_label26_false-unreach-call.c.files/witness.graphml |
witnessSHA | fd1ac18c9bec3a8c47af675c3865e653019e4d6fcb2a29c7a9e0704cce2ea312 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T04:16 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_96000fc8-b902-4cb2-b858-9656b19eb9f3/sv-benchmarks/c/eca-rers2012/Problem03_label26_false-unreach-call.c |
programhash | c73a39be4b04cb22781340db50298b9651d50f3e |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/fd1ac18c9bec3a8c47af675c3865e653019e4d6fcb2a29c7a9e0704cce2ea312.graphml |
witness-sha256 | fd1ac18c9bec3a8c47af675c3865e653019e4d6fcb2a29c7a9e0704cce2ea312 |
witness-size | 1237 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.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/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.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/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.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/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 14 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
3a49a8c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 2 | 2019-12-02 04:04:26 | ||
a85deb2 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 100 | 2019-12-03T22:52 CET (comp) | ||
340c65b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 329 | 2019-12-11T21:44:09+01:00 | 6d9aa1c | |
ea90d85 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 329 | 2019-12-11T21:09:27+01:00 | 3a49a8c | |
53636d0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 329 | 2019-12-11T20:55:24+01:00 | d774fd6 | |
0536ac0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 329 | 2019-12-11T20:44:28+01:00 | 6abe95f | |
f9e4e9e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 331 | 2019-12-08T01:51:23+01:00 | a2d21e8 | |
b367a88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 435 | 2019-12-04T02:58:22+01:00 | a85deb2 | |
3dbf5c5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 329 | 2019-12-03T08:01:04+01:00 | 4f1d880 | |
4f1d880 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 330 | 2019-11-30T13:33:40+01:00 | ||
6d9aa1c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 330 | 2019-11-30T23:35:41+01:00 | ||
11fe345 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 685 | 2019-12-08T00:27:21+01:00 | 9bcb01c | |
cd7433c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 685 | 2019-12-07T21:19:52+01:00 | 52475d5 | |
f82af0a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 685 | 2019-12-05T20:23:00+01:00 | e4593f8 |
Found 16 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
46eff3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2018-12-08T13:38 CET (sv-comp) | ||
89c45b6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 10 | 2018-12-08T03:50:55 | ||
f1e8240 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 108 | 2018-12-07T04:03 CET (sv-comp) | ||
2994ef5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 333 | 2018-12-07T05:19:34+01:00 | ||
5b8e341 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 331 | 2018-12-10T20:37:30+01:00 | 210a332 | |
cadcff6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 329 | 2018-12-09T18:20:38+01:00 | da4d114 | |
f55206b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 330 | 2018-12-08T23:43:17+01:00 | 46eff3f | |
59701c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 329 | 2018-12-08T22:10:17+01:00 | 89c45b6 | |
384673a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 329 | 2018-12-08T08:49:31+01:00 | 2994ef5 | |
a7c28d4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 329 | 2018-12-08T04:50:50+01:00 | ed619a9 | |
29132a9 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 435 | 2018-12-07T17:44:29+01:00 | f1e8240 | |
5c38f42 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 329 | 2018-12-06T10:18:32+01:00 | 759d638 | |
39f5dbf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 329 | 2018-12-06T09:48:08+01:00 | 7a9c568 | |
631eabf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 435 | 2018-12-06T09:13:38+01:00 | 7c2df6f | |
7a9c568 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 330 | 2018-12-05T14:11:09+01:00 | ||
04a610f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 685 | 2018-12-09T20:54:35+01:00 | 2f473f9 |
Found 9 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
28123c0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Veriabs | 3 | 2017-12-02T19:54 CET (sv-comp) | ||
fd1ac18 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 1 | 2017-12-02T04:16 CET (sv-comp) | ||
72627a4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 4 | 2017-12-01T23:47:54.142558 | ||
9a1e004 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 4 | 2017-12-01T11:41:25.088043 | ||
ced0798 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 17 | 2017-12-01T03:19 CET (sv-comp) | ||
5ddcb58 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 187 | 2017-12-01T02:23:11+01:00 | ||
e1ef0dd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26758M | 689 | 2017-11-30T16:01:00+01:00 | ||
99082b1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 122 | 2017-12-01T02:57 CET (sv-comp) | ||
8b2915d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 122 | 2017-11-30T21:08 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem03_label26_false-unreach-call.c, 40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/40ff1c88e431b1b86040d8145a18233cd0c48b8ed0781ea1afb7ce04987def08.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |