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/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c
programSHA 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
witnessName results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c.files/witness.graphml
witnessSHA 28a187f9b4b5e26306aa87c74967cf168e31a2a0b9b95e67dc095f3af3c9b7a8

Information about the Witness from Competition Database

from https://sv-comp.sosy-lab.org/2018/results/witnessInfoByHash/28a187f9b4b5e26306aa87c74967cf168e31a2a0b9b95e67dc095f3af3c9b7a8.json

Key Value
architecture 32bit
creationtime 2017-12-01T14:13 CET (sv-comp)
memoryModel precise
producer ESBMC 3.1
program-sha256 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
programfile /tmp/vcloud-vcloud-master/worker/working_dir_7428905d-c75b-43fa-b6b9-ffb0613967dc/sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c
programhash b58543c5c6c478461bb3678f5712726562def78f
sourcecodelang C
specification CHECK( init(main()), LTL(G ! overflow) )
witness-file witnessFileByHash/28a187f9b4b5e26306aa87c74967cf168e31a2a0b9b95e67dc095f3af3c9b7a8.graphml
witness-sha256 28a187f9b4b5e26306aa87c74967cf168e31a2a0b9b95e67dc095f3af3c9b7a8
witness-size 3435
witness-type correctness_witness

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 49 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2024/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download dbfd1da Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2023-12-03T04:28:09Z
Download e68bc16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-24 4 2023-12-03T17:19:30+01:00
Download 191c134 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2023-12-20T03:37 CET (comp)
Download 9191584 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 3 2023-12-02T15:34:42Z
Download 24ccf03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-12-17T02:59:36Z
Download d6804df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2023-11-29T19:03:20Z
Download 2ba1c9f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2023-11-29T09:04:04Z
Download 4e1657d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 3 2023-12-02T22:35:27Z
Download 9fb12ca Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp24-0-gc2e9465a7) 4 2023-11-30T22:40:33Z
Download 8e97fe5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-20T03:41:15+01:00 Download 191c134
Download 4b95538 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T14:30:04+01:00 Download 7bd4d10
Download 9517e55 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-19T03:02:47+01:00 Download 28f7e14
Download 5ed8bc3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-17T06:12:01+01:00 Download 24ccf03
Download 688487b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-05T14:23:03+01:00 Download b3de809
Download a042d24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T16:29:17+01:00 Download fa4b005
Download 4ed3f8d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T11:23:38+01:00 Download 9191584
Download 22a888c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-04T02:03:09+01:00 Download 58dde2f
Download 4c879fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T18:30:08+01:00 Download e68bc16
Download a40034e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T09:59:47+01:00 Download dbfd1da
Download 342b0b7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-03T05:56:12+01:00 Download 4e1657d
Download 273042b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T22:44:33+01:00 Download b0d791d
Download 788a5a0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T03:49:16+01:00 Download 9fb12ca
Download b48b4ee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-12-01T00:12:59+01:00 Download 126c99b
Download cc41c46 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T11:36:59+01:00 Download 7c36a28
Download 7c36a28 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 3 2023-11-30T07:23:24+01:00
Download beae037 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-30T02:43:48+01:00 Download d6804df
Download 6b9b87a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T18:25:52+01:00 Download 2ba1c9f
Download a3a0db0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.3 4 2023-11-29T07:52:48+01:00 Download 50ce58e
Download 58dde2f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-e677b7cd46+ 4 2023-12-03T20:42:29+01:00
Download 28f7e14 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2023-12-18T21:49:23+01:00
Download a89b9d3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3 2023-12-17T16:19:12+01:00
Download b3de809 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 2 2023-12-05T10:13:04Z
Download fa4b005 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 2 2023-12-04T14:30:16Z
Download b0d791d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Bubaak 3 2023-12-01T19:52:14Z
Download 50ce58e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 3 2023-11-28T19:41:23Z
Download 126c99b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 5 2023-11-30T21:03:02+01:00
Download 815619c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2023-12-17T01:12:58Z
Download a37ca9d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2023-11-29T19:34:26Z
Download e78453d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.3 3 2023-11-30T05:11:47+01:00
Download 2d44c93 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-e677b7cd46+ 3 2023-12-03T18:04:19+01:00
Download 2a6f13d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2023-12-18T17:33:51+01:00
Download 0a3b503 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-05T10:14:30Z
Download c754922 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2023-12-04T10:13:19Z
Download 5910b07 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 3 2023-11-29T05:34:21Z
Download 21b2d53 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 3 2023-11-30T21:25:15+01:00
Download f1920e2 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: aa48f577-114b-484c-8473-cf6dd4b80072 creation_time: '2023-11-28T20:41:23+01:00' producer: name: Automizer version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1acde2c3-bfb9-4435-9438-57edb80d7689/sv-benchmarks/c/termination-crafted/WhileTrue.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_1acde2c3-bfb9-4435-9438-57edb80d7689/sv-benchmarks/c/termination-crafted/WhileTrue.c : 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 4 2023-11-29T07:49:28+01:00
Download db76923 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 8648ea13-3d84-4228-bc28-cef6c45d243a creation_time: '2023-12-02T16:34:42+01:00' producer: name: Taipan version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fcd92158-49de-4b03-a689-b2ce276d7cc9/sv-benchmarks/c/termination-crafted/WhileTrue.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_fcd92158-49de-4b03-a689-b2ce276d7cc9/sv-benchmarks/c/termination-crafted/WhileTrue.c : 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 4 2023-12-04T12:02:25+01:00
Download 80a3a89 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: '2.0' uuid: 58a21ffa-e30b-40de-9862-96238fa47b58 creation_time: '2023-12-02T23:35:27+01:00' producer: name: Kojak version: 0.2.4-dev-0e0057c task: input_files: - /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_da7d8a55-2fc6-45c8-8de3-cf3c07bc2c67/sv-benchmarks/c/termination-crafted/WhileTrue.c input_file_hashes: ? /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_da7d8a55-2fc6-45c8-8de3-cf3c07bc2c67/sv-benchmarks/c/termination-crafted/WhileTrue.c : 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1 specification: |+ CHECK( init(main()), LTL(G ! overflow) ) data_model: 64bit language: C content: [ ] correctness_witness CPAchecker 2.3 4 2023-12-03T05:43:05+01:00
Download fc2bda3 Inspect Inspect
Validate
- entry_type: invariant_set metadata: format_version: "2.0" uuid: 16bd6ea8-6682-40fa-a785-66b87178af23 creation_time: 2023-11-30T22:40:33Z producer: name: Goblint version: tags/svcomp24-0-gc2e9465a7 command_line: '''./goblint'' ''--conf'' ''conf/svcomp24.json'' ''--sets'' ''ana.specification'' ''../../sv-benchmarks/c/properties/no-overflow.prp'' ''--sets'' ''exp.architecture'' ''64bit'' ''../../sv-benchmarks/c/termination-crafted/WhileTrue.c''' task: input_files: - ../../sv-benchmarks/c/termination-crafted/WhileTrue.c input_file_hashes: ../../sv-benchmarks/c/termination-crafted/WhileTrue.c: 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1 data_model: LP64 language: C specification: CHECK( init(main()), LTL(G ! overflow) ) content: [] correctness_witness CPAchecker 2.3 4 2023-12-01T04:34:15+01:00

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 38 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2023/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 254094a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.4.0 3 2022-12-09T10:00:00Z
Download feabad2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2022-12-10T22:06:51+01:00
Download 191c134 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness VeriOover 1 2022-12-12T10:59 CET (comp)
Download 5c3c3ed Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 3 2022-12-14T13:18:36Z
Download aa2ee36 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-25T09:30:29Z
Download b09829c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2022-12-12T12:37:26Z
Download 9ed304d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Mopsa (v1.0~pre2) 3 2022-12-11T12:21:15Z
Download d98b7e3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 3 2022-12-14T20:09:03Z
Download bcc88a9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp23-0-g4f5dcf38f) 4 2022-12-10T06:57:08Z
Download 47f33d5 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:32:10+01:00 Download 191c134
Download 29aae3b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T11:07:04+01:00 Download 5c3c3ed
Download 5dfb0d8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T07:29:14+01:00 Download bc6fbe0
Download 9f2c0f3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T06:34:19+01:00 Download d98b7e3
Download 14cafc4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T05:18:29+01:00 Download b09829c
Download f0faf02 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T03:49:32+01:00 Download 9ed304d
Download 217ea24 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T02:43:50+01:00 Download 8ca1120
Download d3f4194 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-29T00:06:30+01:00 Download d297d15
Download efea734 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:52:47+01:00 Download feabad2
Download 08e3e64 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T22:23:33+01:00 Download bcc88a9
Download 482fd95 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T19:04:38+01:00 Download 8094c40
Download 2ae4c80 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T17:46:19+01:00 Download 254094a
Download 103d9e4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T11:58:28+01:00 Download ef54b52
Download 4cab2bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-28T00:45:50+01:00 Download aa2ee36
Download 2519cee Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 4 2023-01-27T23:12:15+01:00 Download 6ccced7
Download ef54b52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2 3 2022-12-10T19:55:12+01:00
Download 8ca1120 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.2.1-svn-1715bd67dc+ 4 2022-12-12T01:22:34+01:00
Download 8094c40 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-a45b42da2f+ 4 2022-12-10T00:46:00+01:00
Download 6bb78d4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3 2022-12-08T06:23:32+01:00
Download bc6fbe0 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 3 2022-12-13T15:30:33Z
Download 6ccced7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 5 2022-12-08T01:03:27+01:00
Download 9f5cdc7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2022-12-25T10:17:26Z
Download 4c7b55a Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2022-12-12T14:15:14Z
Download f8201c6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2 3 2022-12-10T20:19:49+01:00
Download 68d8946 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.2.1-svn-1715bd67dc+ 3 2022-12-12T01:06:51+01:00
Download 64e3f8c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-a45b42da2f+ 3 2022-12-10T01:19:10+01:00
Download 8d4063b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Bubaak 3 2022-12-08T15:49:34Z
Download c725614 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 3 2022-12-13T17:33:36Z
Download 69bc3dd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 3 2022-12-07T21:38:05+01:00

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 32 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2022/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 4b343a3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) violation_witness frama-c-sv version 0.2.8 3 2021-12-13T20:40:14Z
Download 434c7b9 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness sv-comp-22 4 2021-12-06T14:18:06+01:00
Download 2033baf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 3 2021-12-09T23:30:21Z
Download ad320df Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2021-12-10T18:51:37
Download cfe870b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 3 2021-12-07T15:34:17Z
Download 8147026 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 3 2021-12-10T08:21:19Z
Download a2bf3e7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (tags/svcomp22-0-ge852ac510) 4 2021-12-07T19:55:55Z
Download b062973 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T21:13:34+01:00 Download ad320df
Download 51971d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T17:27:51+01:00 Download 8147026
Download a24c32c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-10T08:49:26+01:00 Download 2033baf
Download 1a7d4af Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-09T15:41:35+01:00 Download 6d3636d
Download b9d4477 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-08T22:08:15+01:00 Download 09d4af1
Download 4381837 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T23:26:55+01:00 Download a2bf3e7
Download 6707562 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T18:53:19+01:00 Download cfe870b
Download e20160b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-07T02:42:54+01:00 Download e006369
Download 1b0b6cf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T14:46:18+01:00 Download 434c7b9
Download e6d4f16 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-06T01:15:45+01:00 Download 77cac6c
Download 170523b Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 4 2021-12-05T20:20:07+01:00 Download 447d4fc
Download 447d4fc Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.1 3 2021-12-05T19:17:17+01:00
Download 09d4af1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 4 2021-12-08T16:50:52+01:00
Download 6d3636d Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2021-12-09T13:24:39+01:00
Download a67b11f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3 2021-12-06T08:46:38+01:00
Download e006369 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 3 2021-12-06T22:30:00Z
Download 77cac6c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 5 2021-12-05T22:48:14+01:00
Download 9e1f9e6 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2021-12-10T18:50:35
Download b8c1b5c Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 3 2021-12-07T16:25:33Z
Download ffcb37b Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.1 3 2021-12-05T15:33:17+01:00
Download 680ef4e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-fe6f522dd3+ 3 2021-12-08T20:09:57+01:00
Download 2e0faf7 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2021-12-09T11:59:47+01:00
Download 00eba3d Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 3 2021-12-06T18:40:35Z
Download 0d1f022 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness AProVE 3 2021-12-05T11:25:46Z
Download af034ff Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 3 2021-12-05T23:33:12+01:00

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 20 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2021/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 6aaf99c Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness frama-c-sv version 0.2.1 3 2020-12-06T23:32:32
Download 22e2548 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-11T15:58:04
Download f750b98 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 2 2020-12-09T02:33:20
Download 659ad52 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Goblint (svcomp21-0-g82e03b87) 4 2020-12-07T15:09:53
Download 018d6d2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-12T01:39:57+01:00 Download 22e2548
Download 7d9cdd7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T22:03:39+01:00 Download d3ed0c6
Download 002d0bf Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T21:31:42+01:00 Download 7fc3cf7
Download a8160e1 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T03:57:24+01:00 Download f750b98
Download d3402b4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-09T01:53:36+01:00 Download 09b671d
Download 8c22435 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-08T07:43:48+01:00 Download d1d0ac2
Download 1dea8c2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-07T21:12:13+01:00 Download 659ad52
Download 5274fdb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-07T00:14:04+01:00 Download 6aaf99c
Download c2afc7a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T16:58:31+01:00 Download 90b36a2
Download f041808 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 4 2020-12-06T13:12:50+01:00 Download d634d31
Download d634d31 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0 3 2020-12-05T15:32:21+01:00
Download d1d0ac2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 2.0.1-svn-eda176372c+ 4 2020-12-08T04:51:19+01:00
Download f0d1409 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2020-12-11T22:56:51
Download 3438db5 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 2 2020-12-09T02:00:48
Download 565dab3 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0 3 2020-12-05T13:59:13+01:00
Download 69ba18f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 2.0.1-svn-eda176372c+ 3 2020-12-08T05:11:22+01:00

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 7 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2020/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 8b74f03 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-memtrack) ) correctness_witness CPAchecker 1.9 3 2019-11-30T02:04:56+01:00
Download d359464 Inspect Inspect
Validate
CHECK( init(main()), LTL(G valid-deref) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T00:17:43+01:00
Download 3b511fa Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.9 3 2019-11-30T10:39:40+01:00
Download 6994f3e Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T00:15:15+01:00
Download ce7d176 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 1 2019-12-01 08:11:03
Download 4178122 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.9 3 2019-11-29T19:26:32+01:00
Download 1b8f45f Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.8-svn-35b8bb3bb3+ 3 2019-12-01T14:55:44+01:00

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 9 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2019/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 65cb215 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2018-12-08T14:23 CET (sv-comp)
Download b6e82c8 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness SMACK 1.9.3 3 2018-12-08T01:54:59
Download b421a67 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn b8d6131600+ 4 2018-12-08T02:28:13+01:00
Download 2cc4400 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.7-svn 29852 4 2018-12-06T07:27:25+01:00
Download b2e62f1 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Symbiotic 1 2018-12-08T08:05 CET (sv-comp)
Download eb8fa01 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn b8d6131600+ 3 2018-12-07T06:49:47+01:00
Download de709bb Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T09:40:48+01:00
Download a9d847e Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-06T07:23:33+01:00
Download 9dfcdde Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.7-svn 29852 3 2018-12-05T09:27:25+01:00

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 13 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2018/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

Show Witness Inspect Validate Specification Result Type Producer Size (kB) Time stamp Input Witness
Download 1c987f7 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Taipan 3 2017-12-03T07:43Z
Download ae6bfc2 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Symbiotic 1 2017-12-03T04:54 CET (sv-comp)
Download 42b6eb3 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Kojak 3 2017-12-03T10:22Z
Download c1d08cb Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 4.6.0 kind 3 2017-12-02T17:45:49.374194
Download 28a187f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness ESBMC 3.1 3 2017-12-01T14:13 CET (sv-comp)
Download e2d9553 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CPAchecker 1.6.1-svn 26773 4 2017-12-01T11:10:15+01:00
Download 9b7f60f Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness CBMC 3 2017-12-01T12:11 CET (sv-comp)
Download 52bc7f4 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness Automizer 3 2017-12-03T10:18Z
Download 1598752 Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! overflow) ) correctness_witness 2LS 5 2017-12-01T10:22 CET (sv-comp)
Download f18e25a Inspect Inspect
Validate
CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) ) correctness_witness ESBMC 3.1 3 2017-12-01T20:49 CET (sv-comp)
Download 589e158 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness CPAchecker 1.6.1-svn 26773 3 2017-12-01T14:52:19+01:00
Download ae6cad8 Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness Automizer 3 2017-12-03T11:17Z
Download e61bccd Inspect Inspect
Validate
CHECK( init(main()), LTL(F end) ) violation_witness 2LS 3 2017-12-01T12:34 CET (sv-comp)

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

Trying to find witnesses for program (2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1, sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c).

Found 0 witnesses for program sv-benchmarks/c/termination-crafted/WhileTrue_true-no-overflow_false-termination_true-valid-memsafety.c, 2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1
from https://sv-comp.sosy-lab.org/2017/results/witnessListByProgramHashJSON/2c915ce64f8b11abacbd175f69c99f9afd8b2edc1142f6db1504c1dcc6414eb1.json

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