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

View and Validate the Witness

Input Given to this Service about the Witness (URL Query)

Key Value
programName sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c
programSHA 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
witnessName results-verified/cbmc.2018-12-04_2248.logfiles/sv-comp19_prop-reachsafety.pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c.files/witness.graphml
witnessSHA 6ebd4c3cceda97d5cb08766ab98a44c9a14335a3345010a78b99f4488f13ca3e

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/6ebd4c3cceda97d5cb08766ab98a44c9a14335a3345010a78b99f4488f13ca3e.json

Key Value
architecture 32bit
creationtime 2018-12-05T13:51 CET (sv-comp)
producer CBMC
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c
programhash 41aeb4b3eafc96a3464e4411965bc0b5575f7ae7
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/6ebd4c3cceda97d5cb08766ab98a44c9a14335a3345010a78b99f4488f13ca3e.graphml
witness-sha256 6ebd4c3cceda97d5cb08766ab98a44c9a14335a3345010a78b99f4488f13ca3e
witness-size 63170
witness-type violation_witness

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

Trying to find witnesses for program (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.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 (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.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 (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.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 (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.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 (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 2dd41f5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 5 2019-12-01 22:08:09
Download 7f9dfa8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 61 2019-12-03T23:21 CET (comp)
Download 61a616b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 75 2019-12-11T21:45:32+01:00 Download e66f46f
Download 458fbaa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 75 2019-12-11T20:54:21+01:00 Download ee3a8b7
Download fdd7b77 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 75 2019-12-11T20:44:41+01:00 Download 39bc61b
Download d2e936a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 75 2019-12-08T01:51:18+01:00 Download f4f2a02
Download b0b34b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 78 2019-12-08T00:26:45+01:00 Download 9032312
Download 3e78dc9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 78 2019-12-07T21:15:55+01:00 Download 174a2a3
Download 001ca55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 75 2019-12-03T08:09:49+01:00 Download eff4e85
Download eff4e85 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 70 2019-11-30T14:25:10+01:00
Download f4f2a02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 57 2019-12-07T20:29:17+01:00
Download e66f46f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 75 2019-12-01T04:49:43+01:00
Download 355487c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 82 2019-12-11T21:09:03+01:00 Download 2dd41f5
Download 59191ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-05T20:20:29+01:00 Download 10f563a
Download 234255e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-05T19:34:08+01:00 Download a3fdd36
Download cf2010c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 83 2019-12-04T02:58:22+01:00 Download 7f9dfa8
Download 59b6a9c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 4 2019-12-01 21:26:45

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

Trying to find witnesses for program (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 17 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download d839160 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 8 2018-12-08T09:20 CET (sv-comp)
Download 0791864 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 28 2018-12-08T13:58:54
Download 5711fd5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 78 2018-12-08T03:05:08+01:00
Download f2a4a3c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 78 2018-12-09T20:53:20+01:00 Download 1a2d368
Download e751cbe Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 78 2018-12-09T20:37:46+01:00 Download c982fe8
Download fe01972 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-09T18:21:27+01:00 Download fd034b7
Download 1783461 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T23:44:44+01:00 Download d839160
Download fe13ac6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T08:15:23+01:00 Download 5711fd5
Download 8d7f1df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T04:55:19+01:00 Download 8e94ebf
Download 68e8ef0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-08T03:57:54+01:00 Download 92df52a
Download e2aa9c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-06T10:17:41+01:00 Download 328968a
Download 4062ed6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 75 2018-12-06T09:48:54+01:00 Download 357d069
Download 357d069 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 70 2018-12-06T07:10:38+01:00
Download e10311e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-10T20:35:14+01:00 Download b0d20a5
Download 05c585b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-08T22:07:43+01:00 Download 0791864
Download 7373baf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-06T09:40:49+01:00 Download 7281d00
Download 8e69542 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 83 2018-12-06T09:18:26+01:00 Download 6ebd4c3

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

Trying to find witnesses for program (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 13 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8e789aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 59 Sat Dec 2 21:59:53 2017
Download 711f1ec Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Taipan 112 2017-12-03T01:42Z
Download 9fe89db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 6 2017-12-02T05:05 CET (sv-comp)
Download 3ed3c10 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 13 2017-12-02T04:44:10.347915
Download af713a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 10 2017-12-01T12:18:39.359402
Download 573e27e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 41 2017-12-01T05:55 CET (sv-comp)
Download 85a54be Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 51 2017-11-30T22:48:21+01:00
Download d33020b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 128 2017-11-30T12:01:59+01:00
Download 68bdc53 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26725 39 2017-12-01T01:16:25+01:00
Download 6b98044 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 41 2017-12-01T22:33:58+01:00
Download 08e9295 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 63 2017-11-30T15:08 CET (sv-comp)
Download afacbd4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Automizer 112 2017-12-02T01:41Z
Download 6dde496 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 64 2017-11-30T14:06 CET (sv-comp)

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

Trying to find witnesses for program (9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280, sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c).

Found 0 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_STARTPALS_ActiveStandby_false-unreach-call.1.ufo.UNBOUNDED.pals.c, 9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/9eaa06e3e18b5546953e93f7118cb23aa8f7c95ce1858d9267fb781882212280.json

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