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.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c
programSHA e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d
witnessName results-validated/cpa-seq-validate-violation-witnesses-pesco.2018-12-08_0739.logfiles/sv-comp19_prop-reachsafety.pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c.files/witness.graphml
witnessSHA e706ad182fea993efc05c17f6410f9fa5a532db074e81eaee14fb4cf3b922c6e

Information about the Witness from Competition Database

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

Key Value
architecture 32bit
creationtime 2018-12-08T09:00:34+01:00
inputwitnesshash a7268c360268db9b85b4cf14a9417eda2aede6de4703527fcd4bae9b2369bbee
producer CPAchecker 1.7-svn 29852
program-sha256 e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d
programfile ../../sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c
programhash e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d
sourcecodelang C
specification CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )
witness-file witnessFileByHash/e706ad182fea993efc05c17f6410f9fa5a532db074e81eaee14fb4cf3b922c6e.graphml
witness-sha256 e706ad182fea993efc05c17f6410f9fa5a532db074e81eaee14fb4cf3b922c6e
witness-size 127716
witness-type violation_witness

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

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

Trying to find witnesses for program (e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c).

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

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

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

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

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c, e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 21cdde0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 6 2019-12-01 11:42:37
Download a761821 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Pinaka 84 2019-12-03T22:06 CET (comp)
Download d1ea09e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 128 2019-12-11T22:00:53+01:00 Download a05f59c
Download f69aca7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 128 2019-12-11T21:46:05+01:00 Download 2a34f55
Download bdbb2e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 123 2019-12-11T21:09:07+01:00 Download 21cdde0
Download 64f467f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 128 2019-12-11T20:44:52+01:00 Download a2f75dc
Download 377534d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 128 2019-12-08T01:52:26+01:00 Download 8dd512e
Download 2e0322c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 123 2019-12-04T02:58:17+01:00 Download a761821
Download d74c741 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / witnessValidation 128 2019-12-03T08:09:50+01:00 Download 1b9b4e7
Download 1b9b4e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.9 / svcomp20 129 2019-11-30T01:08:09+01:00
Download 8dd512e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8 108 2019-12-07T19:33:56+01:00
Download 2a34f55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ / svcomp20-pesco 124 2019-12-01T00:21:17+01:00
Download b785200 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 54 2019-12-11T20:54:50+01:00 Download fbd8afe
Download 3babd04 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 54 2019-12-05T20:21:54+01:00 Download e058408
Download 055baab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.9 / witnessValidation 54 2019-12-05T19:34:18+01:00 Download 0679f5f
Download c136832 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 7 2019-12-02 01:56:08

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

Trying to find witnesses for program (e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c, e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 5ebe138 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 12 2018-12-08T13:16 CET (sv-comp)
Download ae764b6 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness SMACK 1.9.3 37 2018-12-08T17:17:01
Download a7268c3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 126 2018-12-06T23:55:30+01:00
Download c887dd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 132 2018-12-09T20:34:05+01:00 Download b8c4737
Download f851b46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 128 2018-12-09T17:59:56+01:00 Download cd26e8d
Download c45557a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 123 2018-12-08T23:43:56+01:00 Download 5ebe138
Download e706ad1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 128 2018-12-08T09:00:34+01:00 Download a7268c3
Download bc15a51 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 123 2018-12-08T04:59:31+01:00 Download 5ef9760
Download 4e4206a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 123 2018-12-06T10:17:36+01:00 Download 6d0201b
Download 8a24be9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 128 2018-12-06T09:47:57+01:00 Download 1c0833f
Download 1c0833f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.7-svn 29852 129 2018-12-06T03:38:07+01:00
Download 3422071 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 54 2018-12-10T20:37:52+01:00 Download 022a044
Download 7d1e775 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 54 2018-12-08T22:07:29+01:00 Download ae764b6
Download 2adc6c7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 54 2018-12-06T09:42:30+01:00 Download 3aee41a
Download b994fba Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness CPAchecker 1.7-svn 29852 54 2018-12-06T09:08:25+01:00 Download d7ce5f1
Download 1f4b99f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness Symbiotic 1 2018-12-07T23:00 CET (sv-comp)

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

Trying to find witnesses for program (e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c).

Found 16 witnesses for program sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c, e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download aff62db Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness VeriAbs 1.3 100 Sat Dec 2 18:11:22 2017
Download 4a9caab Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Symbiotic 11 2017-12-01T23:10 CET (sv-comp)
Download e712b89 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness Kojak 160 2017-12-02T04:46Z
Download 894510c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 kind 14 2017-12-01T22:01:24.098542
Download 92b2a14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 4.6.0 incr 16 2017-12-01T07:55:45.598402
Download 403fd2d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 46 2017-12-01T21:33 CET (sv-comp)
Download 52c7850 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness ESBMC 3.1 43 2017-11-30T19:33 CET (sv-comp)
Download 7c88d20 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26773 125 2017-12-01T01:56:04+01:00
Download 97e136e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker 1.6.1-svn 26758M 180 2017-12-01T02:39:07+01:00
Download 6270339 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CPAchecker (unknown version) 70 2017-12-02T03:00:07+01:00
Download 0cee70f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness CBMC 106 2017-11-30T13:26 CET (sv-comp)
Download f746832 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) violation_witness 2LS 83 2017-11-30T17:16 CET (sv-comp)
Download 47c3d18 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T21:36:32.666546
Download ff66eaf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 4.6.0 3 2017-12-02T11:47:18.225797
Download 3f33ba7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness CBMC 269 2017-12-01T18:18 CET (sv-comp)
Download ee9bf53 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) correctness_witness 2LS 114 2017-12-01T13:35 CET (sv-comp)

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

Trying to find witnesses for program (e18c8eb7ebebccbc387b6c9a38f9dc99d1dce01ddf27405ab9ec90728199118d, sv-benchmarks/c/seq-mthreaded/pals_floodmax.3_false-unreach-call.1.ufo.BOUNDED-6.pals_true-termination.c).

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

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