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_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c
programSHA e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04
witnessName results-verified/smack.2018-12-07_1913.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c.files/witness.graphml
witnessSHA 5e419b321a1bdeffeb3f7f443d56f6b9f57e847ad7d041a3b864ed53933f5ccc

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2019/results/witnessInfoByHash/5e419b321a1bdeffeb3f7f443d56f6b9f57e847ad7d041a3b864ed53933f5ccc.json

Key Value
architecture 32bit
creationtime 2018-12-08T10:00:24
producer SMACK 1.9.3
program-sha256 e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04
programfile /tmp/vcloud-vcloud-master/worker/working_dir_aa74f971-4612-4217-8aa1-cb4627ee1a9d/sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c
programhash e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/5e419b321a1bdeffeb3f7f443d56f6b9f57e847ad7d041a3b864ed53933f5ccc.graphml
witness-sha256 5e419b321a1bdeffeb3f7f443d56f6b9f57e847ad7d041a3b864ed53933f5ccc
witness-size 67724
witness-type violation_witness

This witness was created for this program (cf. table above, e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04).

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

Trying to find witnesses for program (e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c).

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

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

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

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

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

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 7692882 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 246 2019-12-11T21:55:45+01:00 Download cba2a4e
Download ee52c9c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 256 2019-12-11T20:44:32+01:00 Download 81a7e1f
Download b6e77b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 241 2019-12-08T01:52:24+01:00 Download f740359
Download 7c022e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 243 2019-12-03T08:00:41+01:00 Download a063683
Download a063683 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 254 2019-11-30T11:39:11+01:00
Download f740359 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 198 2019-12-07T13:32:44+01:00
Download cba2a4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 247 2019-12-01T01:56:51+01:00
Download 37348a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 132 2019-12-11T20:54:48+01:00 Download 5b485a1
Download 43922f6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 132 2019-12-05T20:20:31+01:00 Download 35c8442
Download 1971121 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 132 2019-12-05T19:34:10+01:00 Download eaf66f4

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

Trying to find witnesses for program (e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 3326ade Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 18 2018-12-08T13:19 CET (sv-comp)
Download 5e419b3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 68 2018-12-08T10:00:24
Download f1a92a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 248 2018-12-08T00:53:04+01:00
Download e6111a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 256 2018-12-09T18:20:27+01:00 Download ab95392
Download 0adf3e8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 240 2018-12-08T23:42:47+01:00 Download 3326ade
Download 0b72c09 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 246 2018-12-08T08:33:02+01:00 Download f1a92a9
Download a0f1e82 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 243 2018-12-06T09:48:47+01:00 Download 3163bdf
Download 3163bdf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 255 2018-12-06T04:04:19+01:00
Download 3ce64ab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 132 2018-12-10T20:35:14+01:00 Download 19f9c3b
Download ce6ef80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 132 2018-12-08T22:11:09+01:00 Download 5e419b3
Download d7cca4e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 132 2018-12-08T05:04:08+01:00 Download dbdf654
Download ab68164 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 132 2018-12-06T10:17:55+01:00 Download a9cd5fc
Download e7cbc30 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 132 2018-12-06T09:40:40+01:00 Download bc71c6e
Download d98443e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 132 2018-12-06T09:08:54+01:00 Download 8b25be1

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

Trying to find witnesses for program (e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c).

Found 14 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c, e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 84d744a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 198 Sun Dec 3 01:04:06 2017
Download 33ba913 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 16 2017-12-02T01:17 CET (sv-comp)
Download 7de2bba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 309 2017-12-02T09:37Z
Download baed103 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 36 2017-12-02T01:32:49.964961
Download d0c05aa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 38 2017-12-01T15:59:37.331575
Download 11bc618 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 84 2017-12-01T16:52 CET (sv-comp)
Download f43dad8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 81 2017-11-30T23:30 CET (sv-comp)
Download ef18dbb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 243 2017-11-30T16:01:38+01:00
Download db4d8f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 204 2017-11-30T18:37 CET (sv-comp)
Download eab6ff7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 150 2017-11-30T12:37 CET (sv-comp)
Download 74b4138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:53:03.005161
Download 9068929 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T10:22:39.445374
Download 3e4e8d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 500 2017-12-01T15:01 CET (sv-comp)
Download 3c6f806 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 273 2017-12-01T11:42 CET (sv-comp)

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

Trying to find witnesses for program (e167d36a3aaf10d40886aadf0e9acf596cf75777b449c80ce0925d5beeee0e04, sv-benchmarks/c/seq-mthreaded/pals_floodmax.4_false-unreach-call.2.ufo.BOUNDED-8.pals_true-termination.c).

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

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