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 (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).

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

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

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

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

Found 7 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download b691b55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6549 2019-12-11T21:46:22+01:00 Download 0e18e84
Download 8618725 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6548 2019-12-11T20:54:35+01:00 Download 5cee89a
Download a9f1231 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6548 2019-12-11T20:44:52+01:00 Download fa12315
Download fb6c9c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6582 2019-12-08T01:52:27+01:00 Download 62948b1
Download cb497a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 6549 2019-12-03T08:10:29+01:00 Download 46102aa
Download 46102aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 6651 2019-11-30T14:35:32+01:00
Download 0e18e84 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 6611 2019-11-30T23:51:53+01:00

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

Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).

Found 8 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 43d2278 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 6651 2018-12-06T23:57:34+01:00
Download 1a93031 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6582 2018-12-10T20:35:46+01:00 Download f2384bc
Download 7a16d33 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6548 2018-12-09T18:04:00+01:00 Download 5a00acb
Download e37f135 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6549 2018-12-08T09:01:52+01:00 Download 43d2278
Download 209aece Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6549 2018-12-08T05:00:38+01:00 Download 7822c5c
Download b94327b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6549 2018-12-06T10:18:49+01:00 Download 68d7299
Download f754c0d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6549 2018-12-06T09:48:57+01:00 Download 81109d6
Download 81109d6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 6651 2018-12-06T06:48:30+01:00

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

Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).

Found 5 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 896b5f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 5 2017-12-02T04:50:12.968958
Download 2d9c0b5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 5 2017-12-01T17:03:00.548858
Download 61e6b26 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 3647 2017-11-30T18:21:12+01:00
Download fee6c4b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 2393 2017-12-01T02:25 CET (sv-comp)
Download f956f77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 2395 2017-11-30T19:54 CET (sv-comp)

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

Trying to find witnesses for program (67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c, sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c).

Found 0 witnesses for program sv-benchmarks/c/eca-rers2012/Problem05_label26_false-unreach-call.c, 67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/67fced29a5cf0eff58ad5a1fde03eec661661d956d13d56a9bb832dccb2b220c.json

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