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/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c |
programSHA | 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77 |
witnessName | results-verified/symbiotic.2017-12-01_2241.logfiles/sv-comp18.pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA | 10ea9a14a99c4a15e1e78e0b44f7e6485b2ad537660517d2217f01b9a53d6aa5 |
Key | Value |
architecture | 32bit |
creationtime | 2017-12-02T15:43 CET (sv-comp) |
producer | Symbiotic |
program-sha256 | 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77 |
programfile | /tmp/vcloud-vcloud-master/worker/working_dir_9773feeb-48a4-44ce-907c-31b6edaeb3ef/sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c |
programhash | 53989f56751d7cf9cb4f623fbfb17e9fa4a91308 |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/10ea9a14a99c4a15e1e78e0b44f7e6485b2ad537660517d2217f01b9a53d6aa5.graphml |
witness-sha256 | 10ea9a14a99c4a15e1e78e0b44f7e6485b2ad537660517d2217f01b9a53d6aa5 |
witness-size | 7641 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
6416647 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 126 | 2019-12-04T01:06 CET (comp) | ||
a89f1e0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 190 | 2019-12-11T21:57:58+01:00 | 2b727d6 | |
1f86782 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 192 | 2019-12-11T20:44:48+01:00 | 0835108 | |
0017b50 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 190 | 2019-12-03T08:06:24+01:00 | d479008 | |
d479008 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 193 | 2019-11-30T05:16:15+01:00 | ||
2b727d6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 191 | 2019-12-01T00:43:30+01:00 | ||
065edec | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 34 | 2019-12-11T21:09:10+01:00 | 4365ea4 | |
46ce561 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 34 | 2019-12-11T20:54:23+01:00 | 8090464 | |
e4d9c59 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 35 | 2019-12-08T01:52:10+01:00 | f6c7762 | |
27e9222 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 34 | 2019-12-05T20:20:48+01:00 | d754cc2 | |
8cde6c3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 34 | 2019-12-05T19:34:03+01:00 | 20ef100 | |
efb1920 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 36 | 2019-12-04T02:58:24+01:00 | 6416647 | |
9fb426d | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 4 | 2019-12-01 07:55:08 |
Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
65982e7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2018-12-08T09:51 CET (sv-comp) | ||
ed96983 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 50 | 2018-12-08T03:58:39 | ||
24c56a8 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 192 | 2018-12-07T10:23:44+01:00 | ||
cc3cf3f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 190 | 2018-12-08T23:44:34+01:00 | 65982e7 | |
6267c55 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 190 | 2018-12-08T08:42:37+01:00 | 24c56a8 | |
fe2ffa0 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 190 | 2018-12-06T09:47:58+01:00 | 1ba9bf6 | |
1ba9bf6 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 193 | 2018-12-05T15:40:49+01:00 | ||
0aac318 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-10T20:36:04+01:00 | 609811f | |
f9ab775 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-09T18:22:53+01:00 | 1e7a1e6 | |
80be670 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-08T22:08:39+01:00 | ed96983 | |
52b2914 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-08T05:02:22+01:00 | 274c39f | |
b3dd183 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-08T04:30:30+01:00 | be38bd5 | |
758913e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 35 | 2018-12-06T10:20:12+01:00 | 1325041 | |
2cc0389 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-06T09:40:44+01:00 | ffa0945 | |
bdb66a5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 34 | 2018-12-06T09:20:04+01:00 | 5e64978 |
Found 9 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
b4fb9cc | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 128 | Sat Dec 2 20:50:22 2017 | ||
10ea9a1 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 8 | 2017-12-02T15:43 CET (sv-comp) | ||
f2dc545 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 24 | 2017-12-01T16:22:08.585694 | ||
fb5e07a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 24 | 2017-12-01T20:52:51.494792 | ||
f74242b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 61 | 2017-11-30T22:50 CET (sv-comp) | ||
8b115a3 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 189 | 2017-11-30T11:29:04+01:00 | ||
1bfe02c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker (unknown version) | 112 | 2017-12-01T21:03:46+01:00 | ||
3d3ca3e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 134 | 2017-12-01T01:27 CET (sv-comp) | ||
86fc47b | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 111 | 2017-11-30T12:50 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/5de4a549cabb8b6197546490011a94a4d554fdffd13958bd71d995c282eafd77.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |