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 (e08c4cc55033b30c2e32a81f90c641e985e627e843c66525877d3a7ed431dc79, sv-benchmarks/c/eca-rers2012/Problem14_label08_false-unreach-call_false-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 86a3df2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 4 2019-12-01 19:02:06
Download 388474b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 394 2019-12-04T01:09 CET (comp)
Download ba25ea8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1266 2019-12-11T21:09:37+01:00 Download 86a3df2
Download 2fb9ae0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1266 2019-12-11T20:44:32+01:00 Download 2fe6894
Download 971f655 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1577 2019-12-04T02:58:19+01:00 Download 388474b
Download 744b2be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 1266 2019-12-03T08:08:12+01:00 Download 72f0bb0
Download 72f0bb0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 1266 2019-11-30T06:28:39+01:00
Download 7797295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 301 2019-12-11T20:55:01+01:00 Download 169e6ec
Download b98e09e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 301 2019-12-07T21:19:26+01:00 Download 2e93c57
Download 0087ef0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 301 2019-12-05T20:22:39+01:00 Download fc9f029
Download 9336d53 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 23:55:28

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 0f7f75d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2018-12-08T06:15 CET (sv-comp)
Download 1534fe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 461 2018-12-07T07:00 CET (sv-comp)
Download 93c17ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 1272 2018-12-06T20:31:28+01:00
Download 619113b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1267 2018-12-09T18:21:56+01:00 Download 8b4926e
Download 3ca5e8c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1266 2018-12-08T08:58:35+01:00 Download 93c17ae
Download 8870691 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1577 2018-12-07T17:44:32+01:00 Download 1534fe1
Download 37ba7b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1266 2018-12-06T09:48:21+01:00 Download cf5f243
Download 4ebdf69 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1578 2018-12-06T09:09:31+01:00 Download 51ef84e
Download cf5f243 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 1266 2018-12-05T21:40:24+01:00
Download cf6672d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-09T20:53:41+01:00 Download 9e228f3
Download bd0074e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-09T20:38:16+01:00 Download b408174
Download 699cccd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-08T23:45:06+01:00 Download 0f7f75d
Download 5874ee1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-08T04:55:31+01:00 Download 92457e8
Download 74aa9c9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-06T10:10:22+01:00 Download abdac1c
Download 8107509 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 301 2018-12-06T09:43:45+01:00 Download 3f0363c

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5c9c5af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 702 Sat Dec 2 22:58:17 2017
Download 2c48886 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 1 2017-12-02T04:18 CET (sv-comp)
Download b6cb1cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 8 2017-12-01T18:10:12.039385
Download d1e1f3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 8 2017-12-01T20:08:03.577055
Download 925fc30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 22 2017-12-01T21:46 CET (sv-comp)
Download da2748d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 679 2017-11-30T15:28:34+01:00
Download 89063e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 937 2017-11-30T14:41:32+01:00
Download aa48b7c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 677 2017-12-01T01:13:01+01:00
Download 074afe7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 517 2017-11-30T19:35 CET (sv-comp)
Download f9c4d1e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 973 2017-12-02T08:39Z
Download 3882f03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 522 2017-11-30T18:57 CET (sv-comp)
Download f8d8ac1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 147 2017-12-03T11:16Z
Download 2c6522a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 577 2017-12-01T12:25 CET (sv-comp)

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

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

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

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