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 (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.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 (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.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 (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.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 (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.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 (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8e06fad Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 683 2019-12-11T21:43:24+01:00 Download 853255b
Download 4261fef Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 211 2019-12-11T20:44:38+01:00 Download 147f4bb
Download fa0be8f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 212 2019-12-08T01:51:35+01:00 Download 225085e
Download e88f6a2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 211 2019-12-03T08:09:44+01:00 Download d62c29f
Download d62c29f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 220 2019-11-30T06:48:02+01:00
Download 225085e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 196 2019-12-07T15:17:05+01:00
Download 853255b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 684 2019-12-01T07:28:46+01:00
Download 2338af9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 74 2019-12-11T21:09:30+01:00 Download 60ca597
Download dee06c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 74 2019-12-11T20:54:53+01:00 Download 1308921
Download c7acbe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 74 2019-12-07T21:15:19+01:00 Download 46ed62f
Download bbd4d76 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 74 2019-12-05T20:20:35+01:00 Download 054dfa0
Download dcc584c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 74 2019-12-05T19:34:27+01:00 Download cc14a06
Download 4ba4b1d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 5 2019-12-01 06:18:13

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

Trying to find witnesses for program (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6b8ec39 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 9 2018-12-08T02:07 CET (sv-comp)
Download 019754e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 33 2018-12-08T05:49:52
Download 654315f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 696 2018-12-07T18:24:07+01:00
Download d5b850c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 278 2018-12-09T18:20:46+01:00 Download 37a0f1b
Download 2b1745a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 211 2018-12-08T23:43:52+01:00 Download 6b8ec39
Download 45f0e42 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 683 2018-12-08T09:03:07+01:00 Download 654315f
Download 954aba9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 211 2018-12-06T09:48:10+01:00 Download 655cfcd
Download 655cfcd Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 220 2018-12-06T00:35:49+01:00
Download 9a13eda Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-10T20:35:26+01:00 Download 90e24c7
Download 2eea474 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-09T20:39:28+01:00 Download aa3d3c2
Download 1d359e5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-08T22:08:33+01:00 Download 019754e
Download 4225b9a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-08T04:53:40+01:00 Download 3606bb2
Download 1a612a8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-06T10:09:33+01:00 Download c427b5a
Download 1fc5fae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-06T09:41:39+01:00 Download 967c3bd
Download 8c7130e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 74 2018-12-06T09:20:25+01:00 Download b66b6ab

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

Trying to find witnesses for program (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 15 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 546d4ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 115 Sat Dec 2 21:56:57 2017
Download a416335 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 3 2017-12-02T15:45 CET (sv-comp)
Download 6a51486 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 26 2017-12-02T00:43:03.673357
Download 2b233ae Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 18 2017-12-01T14:13:05.645236
Download 8067644 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 105 2017-12-01T20:31 CET (sv-comp)
Download 094d9ba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 79 2017-12-01T04:45 CET (sv-comp)
Download 343507a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 213 2017-11-30T16:59:23+01:00
Download f07cd57 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 305 2017-11-30T12:49:51+01:00
Download 412ffe1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 268 2017-11-30T20:33 CET (sv-comp)
Download c53d6d7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 254 2017-12-02T01:23Z
Download eab0ab3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 95 2017-11-30T18:15 CET (sv-comp)
Download dc0698d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T19:57:06.054376
Download 9c470f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T12:50:57.419296
Download 97c3fe6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 639 2017-12-01T17:48 CET (sv-comp)
Download 60bde2a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 633 2017-12-01T16:06 CET (sv-comp)

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

Trying to find witnesses for program (ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_Triplicated_false-unreach-call.2.ufo.BOUNDED-10.pals_true-termination.c, ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/ad9f534e8d8cbbdc425844aea8a6e288c54e090be1efd7d7920dfac5a0188144.json

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