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-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c |
programSHA | 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2 |
witnessName | results-verified/cbmc.2017-11-30_1120.logfiles/sv-comp18.pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c.files/witness.graphml |
witnessSHA | d13a88e3351a887fcd1d45551e907f6cb29d829a370f8b53132f26b8df356340 |
Key | Value |
architecture | 32bit |
creationtime | 2017-11-30T22:27 CET (sv-comp) |
producer | CBMC |
program-sha256 | 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2 |
programfile | ../../sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c |
programhash | 850d702f76c676e039419a710a30927f0b11322b |
sourcecodelang | C |
specification | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) |
witness-file | witnessFileByHash/d13a88e3351a887fcd1d45551e907f6cb29d829a370f8b53132f26b8df356340.graphml |
witness-sha256 | d13a88e3351a887fcd1d45551e907f6cb29d829a370f8b53132f26b8df356340 |
witness-size | 144956 |
witness-type | violation_witness |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.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-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.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-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.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-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.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-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
658917e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Pinaka | 136 | 2019-12-03T22:25 CET (comp) | ||
5045917 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-11T21:57:22+01:00 | 063f4cf | |
fa7845c | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 198 | 2019-12-11T20:44:40+01:00 | b4e9ea6 | |
a3f9805 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / witnessValidation | 204 | 2019-12-03T08:10:37+01:00 | 5339073 | |
5339073 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.9 / svcomp20 | 208 | 2019-11-29T14:34:16+01:00 | ||
063f4cf | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco | 205 | 2019-11-30T20:26:28+01:00 | ||
99f3495 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-11T21:09:02+01:00 | 9994fe0 | |
fc30e2a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-11T20:55:07+01:00 | 48dead6 | |
ccabaab | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 43 | 2019-12-08T01:51:31+01:00 | 9df4b51 | |
176feb5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 42 | 2019-12-05T20:20:42+01:00 | 728555e | |
1798e65 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-05T19:34:18+01:00 | 72a31b4 | |
ad7d2df | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.9 / witnessValidation | 44 | 2019-12-04T02:58:19+01:00 | 658917e | |
3861b6e | Inspect | CHECK( init(main()), LTL(F end) ) | violation_witness | Symbiotic | 5 | 2019-12-01 04:18:00 |
Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
632c659 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 10 | 2018-12-08T08:55 CET (sv-comp) | ||
2f32b57 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | SMACK 1.9.3 | 50 | 2018-12-08T05:40:49 | ||
1b022b4 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn b8d6131600+ | 206 | 2018-12-07T19:06:54+01:00 | ||
9dd9a88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 198 | 2018-12-09T18:20:39+01:00 | 9f6944d | |
ee99eaa | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 199 | 2018-12-08T23:44:06+01:00 | 632c659 | |
569db14 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-08T08:26:32+01:00 | 1b022b4 | |
d97f94e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 204 | 2018-12-06T09:47:56+01:00 | c47350a | |
c47350a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.7-svn 29852 | 208 | 2018-12-06T00:44:14+01:00 | ||
f1d4e6d | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 43 | 2018-12-10T20:36:18+01:00 | 406846d | |
0354cbd | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-08T22:07:30+01:00 | 2f32b57 | |
216f59f | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 43 | 2018-12-08T04:50:15+01:00 | 1d9ed49 | |
2337811 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 43 | 2018-12-06T10:13:57+01:00 | c18b33f | |
32ddb88 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 44 | 2018-12-06T09:41:31+01:00 | c016cb3 | |
61598f5 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | correctness_witness | CPAchecker 1.7-svn 29852 | 42 | 2018-12-06T09:19:52+01:00 | a88c138 |
Found 8 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |
881f20e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | VeriAbs 1.3 | 141 | Sat Dec 2 23:30:06 2017 | ||
869df67 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | Symbiotic | 10 | 2017-12-01T23:50 CET (sv-comp) | ||
b36960e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 kind | 25 | 2017-12-01T15:04:11.722413 | ||
5de67b7 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 4.6.0 incr | 25 | 2017-12-01T11:38:40.627490 | ||
c673d83 | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | ESBMC 3.1 | 62 | 2017-11-30T21:43 CET (sv-comp) | ||
014cd7a | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CPAchecker 1.6.1-svn 26773 | 200 | 2017-11-30T16:25:15+01:00 | ||
d13a88e | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | CBMC | 145 | 2017-11-30T22:27 CET (sv-comp) | ||
d6d17ae | Inspect | CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) | violation_witness | 2LS | 119 | 2017-12-01T00:04 CET (sv-comp) |
Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_lcr-var-start-time.4_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/6afe8bdd736999b2eca93451c0771da4fcd6a22212721cdeb99c1c66654398a2.json
Show Witness | Inspect | Validate | Specification | Result Type | Producer | Size (kB) | Time stamp | Input Witness |