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).

This link does not point to a witness, but below is a list of witnesses for the same program.

Available Results for the Program from Witness Store SV-COMP '24

Trying to find witnesses for program (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.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 (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.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 (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.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 (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.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 (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 18 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download e25034a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 2 2019-12-02 02:45:22
Download bc74670 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 62 2019-12-03T22:23 CET (comp)
Download 2e5e1ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 187 2019-12-11T21:50:32+01:00 Download da8cbfe
Download 65b06cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 187 2019-12-11T21:09:27+01:00 Download e25034a
Download 4111f12 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 187 2019-12-11T20:55:19+01:00 Download ea8e542
Download 2eb70a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 187 2019-12-11T20:44:48+01:00 Download b709f7a
Download 2abfa65 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 188 2019-12-08T01:51:20+01:00 Download 57678b4
Download 2261f8a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 236 2019-12-04T02:58:04+01:00 Download bc74670
Download 5fc2b7b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 187 2019-12-03T08:10:28+01:00 Download 976cf83
Download 976cf83 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 186 2019-11-30T07:14:49+01:00
Download da8cbfe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 187 2019-12-01T02:39:32+01:00
Download c3efdd6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-11T21:44:34+01:00 Download c54b3c2
Download 67a0497 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-08T00:28:05+01:00 Download 9d9754e
Download 6eed284 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-07T21:18:03+01:00 Download f74a958
Download a12ebcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T20:21:24+01:00 Download f7a8182
Download 2ac7369 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 287 2019-12-05T19:35:09+01:00 Download edaad8f
Download 440d3f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 339 2019-11-30T08:56:26+01:00
Download 4a63412 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 339 2019-12-01T02:01:32+01:00

Available Results for the Program from Witness Store SV-COMP '19

Trying to find witnesses for program (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 23 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6e8a91f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T11:58 CET (sv-comp)
Download e773232 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 8 2018-12-08T11:25:01
Download c187a78 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 72 2018-12-07T13:09 CET (sv-comp)
Download cccf171 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 187 2018-12-07T09:18:47+01:00
Download de53aef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 188 2018-12-10T20:35:15+01:00 Download 52c40ea
Download a81d267 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-09T18:21:16+01:00 Download 21425b3
Download d646ae7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 189 2018-12-08T23:42:10+01:00 Download 6e8a91f
Download ea80bed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-08T22:11:00+01:00 Download e773232
Download ca1d9ea Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-08T08:47:19+01:00 Download cccf171
Download a554abb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-08T04:57:20+01:00 Download bae9ed1
Download 1e6f539 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 236 2018-12-07T17:45:16+01:00 Download c187a78
Download 8c087fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-06T10:19:44+01:00 Download c74a60e
Download 09ede18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 187 2018-12-06T09:48:46+01:00 Download 3d2e986
Download a62fddf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 236 2018-12-06T09:17:41+01:00 Download f8daa5c
Download 3d2e986 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 186 2018-12-05T22:58:41+01:00
Download 2ad3775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:53:35+01:00 Download fd5c8a8
Download 0245677 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:33:57+01:00 Download aff3aa5
Download 237fcd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-09T20:24:11+01:00 Download e062e18
Download 53804ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 287 2018-12-06T09:43:56+01:00 Download e4e6a34
Download d3f8c05 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 339 2018-12-06T13:25:40+01:00
Download 59237c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 336 2018-12-08T08:00:12+01:00
Download 89d813b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 324 2018-12-06T09:48:26+01:00
Download d04e523 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 327 2018-12-05T20:24:08+01:00

Available Results for the Program from Witness Store SV-COMP '18

Trying to find witnesses for program (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 15 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 95225a7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Veriabs 3 2017-12-03T00:16 CET (sv-comp)
Download c8fcef1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T08:44 CET (sv-comp)
Download fc7988c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 160 2017-12-02T15:21Z
Download 4e7a3d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-01T18:13:24.368824
Download 2aae2b8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T09:56:45.167977
Download f30e4af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 13 2017-12-01T21:17 CET (sv-comp)
Download f070ec1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 13 2017-12-01T01:21 CET (sv-comp)
Download 5eb12b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 107 2017-11-30T23:30:49+01:00
Download ab3865b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 266 2017-11-30T17:42:53+01:00
Download 4365a5a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 104 2017-11-30T20:26:30+01:00
Download c8e7cab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 166 2017-12-01T22:43:30+01:00
Download 556de77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 80 2017-11-30T13:54 CET (sv-comp)
Download 88e66a4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 160 2017-12-02T05:49Z
Download f8cc4e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 81 2017-11-30T13:26 CET (sv-comp)
Download a976b64 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 31 2017-12-01T16:40 CET (sv-comp)

Available Results for the Program from Witness Store SV-COMP '17

Trying to find witnesses for program (d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84, sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem01_label38_false-unreach-call_false-termination.c, d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/d03255fb96013d5d390ce13a4418a5a68b36e8e2ee3e34d56278032ebb2d4b84.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness