category-structure.yml 33.7 KB
Newer Older
1
competition: SV-COMP
Dirk Beyer's avatar
Dirk Beyer committed
2
year: 2022
Dirk Beyer's avatar
Dirk Beyer committed
3
4

verifiers:
5
6
7
8
9
10
11
  2ls:
    name: 2LS
    lang: C
    url: https://github.com/diffblue/2ls
    required-ubuntu-packages: []
    jury-member:
      name: Viktor Malík
12
13
      institution: Brno University of Technology
      country: Czechia
14
      url: https://www.fit.vut.cz/person/imalik/.en
15
    code-owner: viktor.malik
Dirk Beyer's avatar
Dirk Beyer committed
16
17
18
19
  aprove:
    name: AProVE
    lang: C
    url: aprove.informatik.rwth-aachen.de
20
21
22
    required-ubuntu-packages:
      - clang
      - mono-runtime
23
      - openjdk-11-jre-headless
Dirk Beyer's avatar
Dirk Beyer committed
24
25
    jury-member:
      name: Jera Hensel
26
27
      institution: RWTH Aachen
      country: Germany
28
      url:
29
    code-owner: jhensel
30
31
32
33
34
35
36
  brick:
    name: BRICK
    lang: C
    url: https://github.com/brick-tool-dev/BRICK-2.0
    required-ubuntu-packages: []
    jury-member:
      name: Lei Bu
37
38
      institution: Nanjing University
      country: China
39
      url:
40
    code-owner: brick-tool-dev
41
42
43
44
45
  cbmc:
    name: CBMC
    lang: C
    url: https://www.cprover.org/cbmc/
    required-ubuntu-packages:
46
      - gcc
47
      - libc6-dev-i386
48
49
    jury-member:
      name: Michael Tautschnig
50
51
      institution: Queen Mary University of London
      country: UK
52
      url: https://www.tautschnig.net/
53
    code-owner: tautschnig
54
55
56
57
  coveriteam-verifier-algo-selection:
    name: CoVeriTeam-Verifier-AlgoSelection
    lang: C
    url: https://gitlab.com/sosy-lab/software/coveriteam
58
59
60
61
62
63
64
65
66
67
    required-ubuntu-packages:
      - python-is-python2
      - python3-numpy
      - clang
      - python2
      - openjdk-11-jre
      - clang-10
      - python3-lxml 
      - gcc
      - libc6-dev-i386
68
69
70
71
72
    jury-member:
      name: Hors Concours
      institution: --
      country: --
      url:
73
    code-owner: skanav
74
75
76
77
  coveriteam-verifier-parallel-portfolio:
    name: CoVeriTeam-Verifier-ParallelPortfolio
    lang: C
    url: https://gitlab.com/sosy-lab/software/coveriteam
78
79
80
81
82
83
84
85
86
87
    required-ubuntu-packages:
      - python-is-python2
      - python3-numpy
      - clang
      - python2
      - openjdk-11-jre
      - clang-10
      - python3-lxml 
      - gcc
      - libc6-dev-i386
88
89
90
91
92
    jury-member:
      name: Hors Concours
      institution: --
      country: --
      url:
93
    code-owner: skanav
94
95
96
97
  cpa-bam-bnb:
    name: CPA-BAM-BnB
    lang: C
    url: https://cpachecker.sosy-lab.org
98
99
    required-ubuntu-packages:
      - openjdk-11-jre-headless
100
    jury-member:
101
102
103
      name: Hors Concours
      institution: --
      country: --
104
      url:
105
    code-owner: p.andrianov
106
107
108
109
110
111
112
113
114
115
116
  cpa-bam-smg:
    name: CPA-BAM-SMG
    lang: C
    url: https://cpachecker.sosy-lab.org
    required-ubuntu-packages:
      - openjdk-11-jre-headless
    jury-member:
      name: Anton Vasilyev
      institution: ISP RAS
      country: Russia
      url:
117
    code-owner: Druidos
118
  cpa-lockator:
119
120
    name: CPALockator
    lang: C
121
    url: https://cpachecker.sosy-lab.org
122
123
    required-ubuntu-packages:
      - openjdk-11-jre-headless
124
    jury-member:
125
126
127
128
      name: Hors Concours
      institution: --
      country: --
      url:
129
    code-owner: p.andrianov
130
131
132
133
134
  cpachecker:
    name: CPAchecker 2.1
    lang: C
    url: https://cpachecker.sosy-lab.org
    required-ubuntu-packages:
135
      - openjdk-11-jre-headless
136
137
    jury-member:
      name: Thomas Bunk
138
139
      institution: LMU Munich
      country: Germany
140
      url: https://www.sosy-lab.org/people/bunk/
141
    code-owner: TBunk
142
143
144
145
  crux:
    name: Crux
    lang: C
    url: https://crux.galois.com/
146
147
    required-ubuntu-packages:
      - openjdk-11-jre-headless
148
149
    jury-member:
      name: Ryan Scott
150
151
      institution: Galois
      country: USA
152
      url: https://ryanglscott.github.io/
153
    code-owner: RyanGlScott
154
155
  cseq:
    name: CSeq
156
157
158
159
160
161
162
163
    lang: C
    url: https://gitlab.com/emersonwds/cseq
    required-ubuntu-packages: []
    jury-member:
      name: Emerson Sales
      institution: Gran Sasso Science Institute
      country: Italy
      url: https://github.com/Emersonwds
164
    code-owner: emersonwds
165
166
167
168
169
170
171
172
173
  dartagnan:
    name: Dartagnan
    lang: C
    url: https://github.com/hernanponcedeleon/Dat3M
    required-ubuntu-packages:
      - clang-11
      - llvm-11
    jury-member:
      name: Hernán Ponce de León
174
175
      institution: Bundeswehr University Munich
      country: Germany
176
      url: https://hernanponcedeleon.github.io
177
    code-owner: hernanponcedeleon
178
179
180
181
182
183
184
  deagle:
    name: Deagle
    lang: C
    url: https://github.com/Misasasa/Deagle
    required-ubuntu-packages: []
    jury-member:
      name: Fei He
185
186
      institution: Tsinghua University
      country: China
187
      url: https://thufv.github.io/team
188
    code-owner: Misasasa
189
190
191
192
193
194
  divine:
    name: DIVINE
    lang: C
    url: https://divine.fi.muni.cz/
    required-ubuntu-packages: []
    jury-member:
195
196
197
      name: Hors Concours
      institution: --
      country: --
198
      url:
199
    code-owner: xlauko
Dirk Beyer's avatar
Dirk Beyer committed
200
201
202
203
204
205
206
207
208
209
  ebf:
    name: EBF
    lang: C
    url: https://github.com/fatimahkj/EBF
    required-ubuntu-packages: []
    jury-member:
      name: Fatimah Aljaafari
      institution: Univeristy of Manchester
      country: UK
      url:
210
    code-owner: fatimahaljaafari
211
212
213
214
  esbmc-incr:
    name: ESBMC-incr
    lang: C
    url: https://esbmc.org/
215
216
    required-ubuntu-packages:
      - python-is-python2
217
    jury-member:
218
219
220
221
      name: Hors Concours
      institution: --
      country: --
      url:
222
    code-owner: feliperodri
223
224
225
226
  esbmc-kind:
    name: ESBMC-kind
    lang: C
    url: http://esbmc.org/
227
228
    required-ubuntu-packages:
      - python-is-python2
229
230
    jury-member:
      name: Rafael Sá Menezes
231
232
      institution: University of Manchester
      country: UK
233
      url:
234
    code-owner: rafaelsamenezes
235
  frama-c-sv:
236
    name: Frama-C-SV
237
    lang: C
238
    url: https://gitlab.com/sosy-lab/software/frama-c-sv
239
240
    required-ubuntu-packages:
      - frama-c-base
241
      - libwhy3-ocaml-dev
242
      - python3-pycparser
243
244
    jury-member:
      name: Martin Spiessl
245
246
      institution: LMU Munich
      country: Germany
247
      url: https://www.sosy-lab.org/people/spiessl/
248
    code-owner: masp
249
250
251
252
253
254
  gazer-theta:
    name: Gazer-Theta
    lang: C
    url: https://github.com/ftsrg/gazer
    required-ubuntu-packages:
      - clang-9
255
256
      - llvm-9
      - openjdk-11-jdk-headless
257
    jury-member:
258
259
260
      name: Hors Concours
      institution: --
      url:
261
    code-owner: AdamZsofi
262
263
264
265
266
267
268
  goblint:
    name: Goblint
    lang: C
    url: https://goblint.in.tum.de/
    required-ubuntu-packages: []
    jury-member:
      name: Simmo Saan
269
270
      institution: University of Tartu
      country: Estonia
271
      url:
272
    code-owner: sim642
273
274
275
276
  graves:
    name: GraVeS
    lang: C
    url: https://github.com/will-leeson/cpachecker
277
    required-ubuntu-packages:
278
      - openjdk-11-jre-headless
279
280
      - llvm-11
      - clang-11      
281
282
283
284
285
    jury-member:
      name: Will Leeson
      institution: University of Virginia
      country: United States of America
      url: https://will-leeson.github.io/
286
    code-owner: will-leeson
Matthias Kettl's avatar
Matthias Kettl committed
287
  infer:
Dirk Beyer's avatar
Dirk Beyer committed
288
    name: Infer
Matthias Kettl's avatar
Matthias Kettl committed
289
290
    lang: C
    url: https://fbinfer.com/
291
    required-ubuntu-packages: []
Matthias Kettl's avatar
Matthias Kettl committed
292
    jury-member:
293
294
295
      name: Hors Concours
      institution: --
      country: --
Matthias Kettl's avatar
Matthias Kettl committed
296
      url:
297
    code-owner: matthiaskettl
298
299
300
301
302
303
304
  korn:
    name: Korn
    lang: C
    url: https://github.com/gernst/korn
    required-ubuntu-packages: []
    jury-member:
      name: Gidon Ernst
305
306
      institution: LMU Munich
      country: Germany
307
      url: https://www.sosy-lab.org/people/ernst/
308
    code-owner: gernst
Henrich Lauko's avatar
Henrich Lauko committed
309
310
311
312
313
314
315
  lart:
    name: LART
    lang: C
    url: https://github.com/xlauko/lart
    required-ubuntu-packages:
      - clang-12
      - llvm-12
Henrich Lauko's avatar
Henrich Lauko committed
316
      - libz3-4
Henrich Lauko's avatar
Henrich Lauko committed
317
318
319
320
321
322
323
      - python3
      - python3-lxml
    jury-member:
      name: Henrich Lauko
      institution: Masaryk University, Brno
      country: Czechia
      url: https://xlauko.github.io/ 
324
    code-owner: xlauko
325
326
327
328
329
330
  lazycseq:
    name: Lazy-CSeq
    lang: C
    url: https://github.com/omainv/cseq/releases
    required-ubuntu-packages: []
    jury-member:
331
332
333
334
      name: Hors Concours
      institution: --
      country: --
      url:
335
    code-owner: omainv
336
337
338
339
340
341
342
343
344
  locksmith:
    name: Locksmith
    lang: C
    url: http://www.cs.umd.edu/projects/PL/locksmith/
    required-ubuntu-packages: []
    jury-member:
      name: Vesal Vojdani
      institution: University of Tartu
      country: Estonia
345
      url:
346
    code-owner: vesal.vojdani
347
348
349
350
351
352
353
  pesco:
    name: PeSCo
    lang: C
    url: https://github.com/cedricrupb/cpachecker
    required-ubuntu-packages: []
    jury-member:
      name: Cedric Richter
354
355
      institution: Paderborn University
      country: Germany
356
      url: https://en.cs.uni-paderborn.de/sms/team/people/cedric-richter
357
    code-owner: cedricrupb
358
359
360
361
362
363
  pinaka:
    name: Pinaka
    lang: C
    url: https://github.com/sbjoshi/Pinaka
    required-ubuntu-packages: []
    jury-member:
364
365
366
367
      name: Hors Concours
      institution: --
      country: --
      url:
368
    code-owner: akashbanerjeeab
369
370
371
372
  predatorhp:
    name: PredatorHP
    lang: C
    url: https://www.fit.vutbr.cz/research/groups/verifit/tools/predator-hp/
373
374
375
376
    required-ubuntu-packages:
      - expect
      - gcc-7-multilib
      - python-is-python2
377
378
    jury-member:
      name: Hors Concours
379
380
      institution: --
      country: --
381
      url:
382
    code-owner: masp
383
384
385
386
387
388
  sesl:
    name: SESL
    lang: C
    url: https://spencerl-y.github.io/SESL/
    required-ubuntu-packages:
      - clang
389
      - libssl1.1
390
391
392
      - llvm
    jury-member:
      name: Xie Li
393
394
      institution: Academy of Sciences
      country: China
395
      url:
396
    code-owner: SpencerL-Y
397
398
399
400
401
402
403
  smack:
    name: SMACK
    lang: C
    url: https://smackers.github.io/
    required-ubuntu-packages:
      - clang-10
    jury-member:
404
405
406
407
      name: Hors Concours
      institution: --
      country: --
      url:
408
    code-owner: zrakamar
409
410
411
412
413
414
  symbiotic:
    name: Symbiotic
    lang: C
    url: https://github.com/staticafi/symbiotic
    required-ubuntu-packages:
      - python3
415
      - python3-lxml
416
417
    jury-member:
      name: Marek Chalupa
418
419
      institution: Masaryk University, Brno
      country: Czechia
420
      url:
421
    code-owner: mchalupa
422
423
424
425
426
427
428
  theta:
    name: Theta
    lang: C
    url: https://github.com/ftsrg/theta
    required-ubuntu-packages:
      - openjdk-11-jre-headless
      - libgomp1
429
      - libmpfr6
430
431
432
433
434
    jury-member:
      name: Vince Molnár
      institution: Budapest University of Technology and Economics
      country: Hungary
      url:
435
    code-owner: AdamZsofi
436
437
438
439
  uautomizer:
    name: UAutomizer
    lang: C
    url: https://ultimate.informatik.uni-freiburg.de
440
441
    required-ubuntu-packages:
      - openjdk-11-jre-headless
442
443
    jury-member:
      name: Matthias Heizmann
444
445
      institution: University of Freiburg
      country: Germany
446
      url: https://swt.informatik.uni-freiburg.de/staff/heizmann
447
    code-owner: danieldietsch
Daniel Dietsch's avatar
Daniel Dietsch committed
448
449
  ugemcutter:
    name: UGemCutter
450
451
    lang: C
    url: https://ultimate.informatik.uni-freiburg.de
Daniel Dietsch's avatar
Daniel Dietsch committed
452
453
    required-ubuntu-packages:
      - openjdk-11-jre-headless
454
455
    jury-member:
      name: Dominik Klumpp
456
457
      institution: University of Freiburg
      country: Germany
458
      url: https://swt.informatik.uni-freiburg.de/staff/klumpp
459
    code-owner: danieldietsch
460
461
462
463
  ukojak:
    name: UKojak
    lang: C
    url: https://ultimate.informatik.uni-freiburg.de
464
465
    required-ubuntu-packages:
      - openjdk-11-jre-headless
466
    jury-member:
467
      name: Frank Schüssele
468
469
      institution: University of Freiburg
      country: Germany
470
      url: https://swt.informatik.uni-freiburg.de/staff/schuessele
471
    code-owner: danieldietsch
472
473
474
475
  utaipan:
    name: UTaipan
    lang: C
    url: https://ultimate.informatik.uni-freiburg.de
476
477
    required-ubuntu-packages:
      - openjdk-11-jre-headless
478
479
    jury-member:
      name: Daniel Dietsch
480
481
      institution: University of Freiburg
      country: Germany
482
      url: https://swt.informatik.uni-freiburg.de/staff/dietsch
483
    code-owner: danieldietsch
484
485
486
487
488
  veriabs:
    name: VeriAbs
    lang: C
    url: https://www.tcs.com/designing-complex-intelligent-systems
    required-ubuntu-packages:
489
      - clang-6.0
490
      - libc6-dev-i386
491
      - llvm-6.0
492
      - openjdk-8-jre-headless
493
      - python-is-python2
494
495
    jury-member:
      name: Priyanka Darke
496
497
      institution: Tata Consultancy Services
      country: India
498
      url:
499
    code-owner: sakshiagrawal1812
Dirk Beyer's avatar
Dirk Beyer committed
500
501
502
503
504
  verifuzz:
    name: VeriFuzz
    lang: C
    url: https://gitlab.com/raveenkm/archives-2021/-/tree/master/2021
    required-ubuntu-packages:
505
      - clang-12
506
      - frama-c-base
Dirk Beyer's avatar
Dirk Beyer committed
507
508
      - gcc-multilib
      - libc6-dev-i386
509
510
511
      - libwhy3-ocaml-dev
      - llvm-12
      - openjdk-8-jdk-headless
Dirk Beyer's avatar
Dirk Beyer committed
512
513
514
      - python2
      - python3-sklearn
      - python3-pandas
515
      - why3
Dirk Beyer's avatar
Dirk Beyer committed
516
517
518
519
520
    jury-member:
      name: Raveendra Kumar Medicherla
      institution: Tata Consultancy Services
      country: India
      url:
521
    code-owner: m.raveendra.kumar
522
523
524
525
526
527
528
  coastal:
    name: COASTAL
    lang: Java
    url: https://www.cs.sun.ac.za/coastal
    required-ubuntu-packages: []
    jury-member:
      name: Hors Concours
529
      institution: --
530
      url:
531
    code-owner: jacogeld
Malte Mues's avatar
Malte Mues committed
532
533
534
535
  gdart:
    name: GDart
    lang: Java
    url: https://github.com/tudo-aqua/gdart-svcomp
536
537
    required-ubuntu-packages:
      - openjdk-11-jre-headless
Malte Mues's avatar
Malte Mues committed
538
539
540
541
542
    jury-member:
      name: Falk Howar
      institution: TU Dortmund
      country: Germany
      url: https://falkhowar.de
543
544
545
    code-owner:
      - fhowar
      - mmuesly
546
547
548
549
550
551
552
  java-ranger:
    name: Java-Ranger
    lang: Java
    url: https://github.com/vaibhavbsharma/java-ranger
    required-ubuntu-packages: []
    jury-member:
      name: Soha Hussein
553
554
      institution: University of Minnesota
      country: USA
555
      url: https://www.linkedin.com/in/sohahusse/
556
    code-owner: soha3
557
558
559
560
561
  jayhorn:
    name: JayHorn
    lang: Java
    url: https://github.com/jayhorn/jayhorn
    required-ubuntu-packages:
562
      - openjdk-8-jdk-headless
563
    jury-member:
564
565
      name: Ali Shamakhi
      institution: Tehran Institute for Advanced Studies
566
      country: Iran
567
      url:
568
    code-owner: ali-shamakhi
569
570
571
572
573
574
575
  jbmc:
    name: JBMC
    lang: Java
    url: https://github.com/diffblue/cbmc
    required-ubuntu-packages: []
    jury-member:
      name: Peter Schrammel
576
577
      institution: University of Sussex and Diffblue
      country: UK
578
      url: http://www.schrammel.it
579
    code-owner: peterschrammel
580
581
582
583
  jdart:
    name: JDart
    lang: Java
    url: https://github.com/tudo-aqua/jdart
584
585
    required-ubuntu-packages:
      - openjdk-11-jre-headless
586
587
    jury-member:
      name: Falk Howar
588
589
      institution: TU Dortmund
      country: Germany
590
      url: https://falkhowar.de
591
592
593
    code-owner:
      - fhowar
      - mmuesly
594
595
596
597
598
599
600
  spf:
    name: SPF
    lang: Java
    url: https://github.com/SymbolicPathFinder/jpf-symbc
    required-ubuntu-packages: []
    jury-member:
      name: Hors Concours
601
602
      institution: --
      country: --
603
      url:
604
    code-owner: yannicnoller
605

606
validators:
607
608
609
610
611
612
613
614
615
616
  cpachecker-validate-correctness-witnesses:
    name: CPAchecker
    lang: C
    url: https://cpachecker.sosy-lab.org/
    required-ubuntu-packages: []
    jury-member:
      name: Thomas Bunk
      institution: LMU Munich
      country: Germany
      url: https://www.sosy-lab.org/people/bunk/
617
    code-owner: TBunk
618
619
620
621
622
623
624
625
626
627
  cpachecker-validate-violation-witnesses:
    name: CPAchecker
    lang: C
    url: https://cpachecker.sosy-lab.org/
    required-ubuntu-packages: []
    jury-member:
      name: Thomas Bunk
      institution: LMU Munich
      country: Germany
      url: https://www.sosy-lab.org/people/bunk/
628
    code-owner: TBunk
629
  cpa-witness2test-validate-violation-witnesses:
630
631
632
633
634
635
636
637
638
    name: CPA-witness2test
    lang: C
    url: https://cpachecker.sosy-lab.org/
    required-ubuntu-packages: []
    jury-member:
      name: Thomas Lemberger
      institution: LMU Munich
      country: Germany
      url: https://www.sosy-lab.org/people/lemberger/
639
    code-owner: TBunk
640
641
642
643
  dartagnan-validate-violation-witnesses:
    name: Dartagnan
    lang: C
    url: https://github.com/hernanponcedeleon/Dat3M
Anthonysdu's avatar
Anthonysdu committed
644
    required-ubuntu-packages:
645
646
      - clang-11
      - llvm-11
Anthonysdu's avatar
Anthonysdu committed
647
    jury-member:
648
649
650
651
      name: Hernán Ponce de León
      institution: Bundeswehr University Munich
      country: Germany
      url: https://hernanponcedeleon.github.io
652
    code-owner: hernanponcedeleon
653
654
655
656
657
658
659
660
661
662
663
664
  fshell-witness2test-validate-violation-witnesses:
    name: CBMC
    lang: C
    url: https://www.cprover.org/cbmc/
    required-ubuntu-packages:
      - gcc
      - libc6-dev-i386
    jury-member:
      name: Michael Tautschnig
      institution: Queen Mary University of London
      country: UK
      url: https://www.tautschnig.net/
665
    code-owner: tautschnig
666
667
668
669
670
  gwit-validate-violation-witnesses:
    name: GWIT
    lang: Java
    url: https://github.com/tudo-aqua/gwit
    required-ubuntu-packages:
671
     - openjdk-11-jre-headless
672
673
674
675
676
    jury-member:
      name: Falk Howar
      institution: TU Dortmund University
      country: Germany
      url: https://falkhowar.de
677
678
679
    code-owner:
      - fhowar
      - mmuesly
680
681
682
683
684
685
686
687
688
689
  metaval-validate-correctness-witnesses:
    name: MetaVal
    lang: C
    url: https://gitlab.com/sosy-lab/software/metaval
    required-ubuntu-packages: []
    jury-member:
      name: Martin Spiessl
      institution: LMU Munich
      country: Germany
      url: https://www.sosy-lab.org/people/spiessl/
690
    code-owner: masp
691
692
693
694
695
696
697
698
699
700
  metaval-validate-violation-witnesses:
    name: MetaVal
    lang: C
    url: https://gitlab.com/sosy-lab/software/metaval
    required-ubuntu-packages: []
    jury-member:
      name: Martin Spiessl
      institution: LMU Munich
      country: Germany
      url: https://www.sosy-lab.org/people/spiessl/
701
    code-owner: masp
702
703
704
705
706
707
708
709
710
711
  nitwit-validate-violation-witnesses:
    name: NITWIT
    lang: C
    url: https://github.com/moves-rwth/nitwit-validator/
    required-ubuntu-packages: []
    jury-member:
      name: Jana (Philipp) Berger
      institution: RWTH Aachen
      country: Germany
      url: https://moves.rwth-aachen.de/people/berger/
712
    code-owner: blizzard4591
713
  symbiotic-witch-validate-violation-witnesses:
714
715
716
717
718
719
720
721
722
723
    name: Symbiotic-Witch
    lang: C
    url: https://github.com/staticafi/symbiotic
    required-ubuntu-packages:
      - python3
    jury-member:
      name: Paulína Ayaziová
      institution: Masaryk University, Brno
      country: Czechia
      url: 
724
    code-owner: mchalupa
725
726
727
728
729
730
731
732
733
734
735
  uautomizer-validate-correctness-witnesses:
    name: UAutomizer
    lang: C
    url: https://ultimate.informatik.uni-freiburg.de
    required-ubuntu-packages:
      - openjdk-11-jre-headless
    jury-member:
      name: Daniel Dietsch
      institution: University of Freiburg
      country: Germany
      url: https://swt.informatik.uni-freiburg.de/staff/dietsch
736
    code-owner: danieldietsch
737
738
739
740
741
742
743
744
745
746
747
  uautomizer-validate-violation-witnesses:
    name: UAutomizer
    lang: C
    url: https://ultimate.informatik.uni-freiburg.de
    required-ubuntu-packages:
      - openjdk-11-jre-headless
    jury-member:
      name: Daniel Dietsch
      institution: University of Freiburg
      country: Germany
      url: https://swt.informatik.uni-freiburg.de/staff/dietsch
748
    code-owner: danieldietsch
749
750
751
752
753
754
755
756
757
758
759
  wit4java-validate-violation-witnesses:
    name: WIT4JAVA
    lang: Java
    url: https://github.com/Anthonysdu/wit4java
    required-ubuntu-packages:
     - python3-networkx
    jury-member:
      name: --
      institution: --
      country: --
      url: 
760
    code-owner: Anthonysdu
761
762
763
764
765
766
767
768
769
770
  witnesslint-validate-witnesses:
    name: WitnessLint
    lang: C
    url: https://github.com/sosy-lab/sv-witnesses
    required-ubuntu-packages: []
    jury-member:
      name: Martin Spiessl
      institution: LMU Munich
      country: Germany
      url: https://www.sosy-lab.org/people/spiessl/
771
    code-owner: masp
772

773

774

775
776
777
# Verifiers participating hors concours are executed and listed in the final results,
# but can not win any medals
hors_concours:
778
  - coastal
779
780
  - coveriteam-verifier-algo-selection
  - coveriteam-verifier-parallel-portfolio
781
782
  - cpa-bam-bnb
  - cpalockator
783
784
  - divine
  - esbmc-incr
785
  - gazer-theta
786
  - lazycseq
787
  - pinaka
788
  - predatorhp
789
  - smack
790
791
  - spf

792

793
794
not_participating:
  - blast
795
796
797
798
  - cbmc-path
  - ceagle
  - civl
  - consequence
799
  - cpa-bam-slicing
800
  - cpa-kind
801
802
  - cpa-par
  - cpa-par-aws
803
804
805
806
807
  - cpa-undef-func
  - depthk
  - divine-explicit
  - divine-smt
  - esbmc-falsi
808
809
  - esbmc-par
  - esbmc-par-aws
810
  - gacal
811
812
813
814
815
816
  - forester
  - hiptnt
  - interpchecker
  - jpf
  - lazycseqabs
  - lazycseqswarm
817
  - map2check
818
819
820
821
822
  - mucseq
  - skink
  - symdivine
  - ulcseq
  - viap
823
  - yogar-cbmc
824
  - yogar-cbmc-parallel
825

826
827
# Properties used in the competition
properties:
828
829
830
831
832
833
834
  - no-overflow
  - termination
  - unreach-call
  - no-data-race
  - valid-memcleanup
  - valid-memsafety
  - assert_java
835
836
837

# scores in demo categories are not counted towards the Overall score
demo_categories:
838
  - no-data-race.NoDataRace-Main
839

Dirk Beyer's avatar
Dirk Beyer committed
840
841
categories:
  ReachSafety:
842
    properties: unreach-call
Dirk Beyer's avatar
Dirk Beyer committed
843
    categories:
Thomas Lemberger's avatar
Thomas Lemberger committed
844
845
846
847
848
849
850
851
852
853
854
855
      - unreach-call.ReachSafety-Arrays
      - unreach-call.ReachSafety-BitVectors
      - unreach-call.ReachSafety-ControlFlow
      - unreach-call.ReachSafety-ECA
      - unreach-call.ReachSafety-Floats
      - unreach-call.ReachSafety-Heap
      - unreach-call.ReachSafety-Loops
      - unreach-call.ReachSafety-ProductLines
      - unreach-call.ReachSafety-Recursive
      - unreach-call.ReachSafety-Sequentialized
      - unreach-call.ReachSafety-XCSP
      - unreach-call.ReachSafety-Combinations
Dirk Beyer's avatar
Dirk Beyer committed
856
857
858
    verifiers:
      - 2ls
      - cbmc
859
860
      - coveriteam-verifier-algo-selection
      - coveriteam-verifier-parallel-portfolio
861
      - cpachecker
Ryan Scott's avatar
Ryan Scott committed
862
      - crux
Dirk Beyer's avatar
Dirk Beyer committed
863
      - divine
864
      - esbmc-kind
865
      - frama-c-sv
866
      - goblint
867
      - graves
868
      - infer
Henrich Lauko's avatar
Henrich Lauko committed
869
      - lart
Dirk Beyer's avatar
Dirk Beyer committed
870
871
872
      - pesco
      - pinaka
      - symbiotic
873
      - theta
Dirk Beyer's avatar
Dirk Beyer committed
874
875
876
877
      - uautomizer
      - ukojak
      - utaipan
      - veriabs
Dirk Beyer's avatar
Dirk Beyer committed
878
      - verifuzz
Dirk Beyer's avatar
Dirk Beyer committed
879
    validators:
Dirk Beyer's avatar
Dirk Beyer committed
880
      - witnesslint
881
882
      - cpachecker-correctness
      - cpachecker-violation
Dirk Beyer's avatar
Dirk Beyer committed
883
884
885
886
887
888
889
      - cpa-witness2test-violation
      - fshell-witness2test-violation
      - nitwit-violation
      - uautomizer-correctness
      - uautomizer-violation
      - metaval-violation
      - metaval-correctness
890
      - symbiotic-witch
Dirk Beyer's avatar
Dirk Beyer committed
891
892

  MemSafety:
893
894
895
    properties:
      - valid-memsafety
      - valid-memcleanup
Dirk Beyer's avatar
Dirk Beyer committed
896
    categories:
Thomas Lemberger's avatar
Thomas Lemberger committed
897
898
899
900
901
902
      - valid-memsafety.MemSafety-Arrays
      - valid-memsafety.MemSafety-Heap
      - valid-memsafety.MemSafety-LinkedLists
      - valid-memsafety.MemSafety-Other
      - valid-memcleanup.MemSafety-MemCleanup
      - valid-memsafety.MemSafety-Juliet
Dirk Beyer's avatar
Dirk Beyer committed
903
904
905
    verifiers:
      - 2ls
      - cbmc
906
      - coveriteam-verifier-parallel-portfolio
907
      - cpa-bam-smg
908
      - cpachecker
Dirk Beyer's avatar
Dirk Beyer committed
909
      - divine
910
      - esbmc-kind
911
      - goblint
912
      - graves
Dirk Beyer's avatar
Dirk Beyer committed
913
914
      - pesco
      - predatorhp
Xie Li's avatar
Xie Li committed
915
      - sesl
Dirk Beyer's avatar
Dirk Beyer committed
916
917
918
919
      - symbiotic
      - uautomizer
      - ukojak
      - utaipan
Dirk Beyer's avatar
Dirk Beyer committed
920
      - verifuzz
Dirk Beyer's avatar
Dirk Beyer committed
921
    validators:
Dirk Beyer's avatar
Dirk Beyer committed
922
      - witnesslint
923
      - cpachecker-violation
Dirk Beyer's avatar
Dirk Beyer committed
924
925
926
927
928
929
      - cpa-witness2test-violation
      - fshell-witness2test-violation
      - uautomizer-correctness
      - uautomizer-violation
      - metaval-violation
      - metaval-correctness
930
      - symbiotic-witch
Dirk Beyer's avatar
Dirk Beyer committed
931
932

  ConcurrencySafety:
933
934
935
    properties:
      - unreach-call
      - no-data-race
Dirk Beyer's avatar
Dirk Beyer committed
936
    categories:
Thomas Lemberger's avatar
Thomas Lemberger committed
937
938
      - unreach-call.ConcurrencySafety-Main
      - no-data-race.NoDataRace-Main
Dirk Beyer's avatar
Dirk Beyer committed
939
940
941
    verifiers:
      - 2ls
      - cbmc
Sudeep Kanav's avatar
Sudeep Kanav committed
942
943
      - coveriteam-verifier-algo-selection
      - coveriteam-verifier-parallel-portfolio
Dirk Beyer's avatar
Dirk Beyer committed
944
      - cpa-lockator
945
      - cpachecker
946
      - cseq
Dirk Beyer's avatar
Dirk Beyer committed
947
      - dartagnan
Misasasa's avatar
Misasasa committed
948
      - deagle
Dirk Beyer's avatar
Dirk Beyer committed
949
      - divine
Dirk Beyer's avatar
Dirk Beyer committed
950
      - ebf
951
952
953
      - esbmc-incr
      - esbmc-kind
      - goblint
954
      - graves
955
      - infer
956
      - lazycseq
Dirk Beyer's avatar
Dirk Beyer committed
957
958
      - pesco
      - symbiotic
959
      - theta
Dirk Beyer's avatar
Dirk Beyer committed
960
      - uautomizer
Daniel Dietsch's avatar
Daniel Dietsch committed
961
      - ugemcutter
Dirk Beyer's avatar
Dirk Beyer committed
962
963
      - ukojak
      - utaipan
Dirk Beyer's avatar
Dirk Beyer committed
964
      - verifuzz
Dirk Beyer's avatar
Dirk Beyer committed
965
966

  NoOverflows:
967
    properties: no-overflow
Dirk Beyer's avatar
Dirk Beyer committed
968
    categories:
Thomas Lemberger's avatar
Thomas Lemberger committed
969
970
      - no-overflow.NoOverflows-BitVectors
      - no-overflow.NoOverflows-Other
Dirk Beyer's avatar
Dirk Beyer committed
971
972
973
    verifiers:
      - 2ls
      - cbmc
974
      - coveriteam-verifier-parallel-portfolio
975
      - cpachecker
Ryan Scott's avatar
Ryan Scott committed
976
      - crux
Dirk Beyer's avatar
Dirk Beyer committed
977
      - divine
978
      - esbmc-kind
979
      - frama-c-sv
Simmo Saan's avatar
Simmo Saan committed
980
      - goblint
981
      - graves
982
      - infer
Dirk Beyer's avatar
Dirk Beyer committed
983
984
985
986
987
988
      - pesco
      - pinaka
      - symbiotic
      - uautomizer
      - ukojak
      - utaipan
Dirk Beyer's avatar
Dirk Beyer committed
989
      - verifuzz
Dirk Beyer's avatar
Dirk Beyer committed
990
    validators:
Dirk Beyer's avatar
Dirk Beyer committed
991
      - witnesslint
992
      - cpachecker-violation
Dirk Beyer's avatar
Dirk Beyer committed
993
994
995
996
997
998
      - cpa-witness2test-violation
      - fshell-witness2test-violation
      - uautomizer-correctness
      - uautomizer-violation
      - metaval-violation
      - metaval-correctness
999
      - symbiotic-witch
Dirk Beyer's avatar
Dirk Beyer committed
1000
1001

  Termination:
1002
    properties: termination
Dirk Beyer's avatar
Dirk Beyer committed
1003
    categories:
1004
      - termination.Termination-BitVectors
Thomas Lemberger's avatar
Thomas Lemberger committed
1005
1006
1007
      - termination.Termination-MainControlFlow
      - termination.Termination-MainHeap
      - termination.Termination-Other
Dirk Beyer's avatar
Dirk Beyer committed
1008
1009
    verifiers:
      - 2ls
Dirk Beyer's avatar
Dirk Beyer committed
1010
      - aprove
Dirk Beyer's avatar
Dirk Beyer committed
1011
      - cbmc
1012
      - coveriteam-verifier-parallel-portfolio
1013
      - cpachecker
Dirk Beyer's avatar
Dirk Beyer committed
1014
      - divine
1015
      - esbmc-kind
1016
      - goblint
1017
      - graves
Dirk Beyer's avatar
Dirk Beyer committed
1018
1019
1020
1021
1022
1023
      - pesco
      - pinaka
      - symbiotic
      - uautomizer
      - ukojak
      - utaipan
Dirk Beyer's avatar
Dirk Beyer committed
1024
      - verifuzz
Dirk Beyer's avatar
Dirk Beyer committed
1025
    validators:
Dirk Beyer's avatar
Dirk Beyer committed
1026
      - witnesslint
1027
      - cpachecker-violation
Dirk Beyer's avatar
Dirk Beyer committed
1028
1029
1030
1031
      - uautomizer-violation
      - metaval-violation

  SoftwareSystems:
1032
1033
1034
1035
    properties:
      - unreach-call
      - no-overflow
      - valid-memsafety
Dirk Beyer's avatar
Dirk Beyer committed
1036
    categories:
Thomas Lemberger's avatar
Thomas Lemberger committed
1037
      - unreach-call.SoftwareSystems-AWS-C-Common-ReachSafety
1038
      - unreach-call.SoftwareSystems-BusyBox-ReachSafety
Thomas Lemberger's avatar
Thomas Lemberger committed
1039
1040
1041
1042
1043
1044
1045
1046
      - valid-memsafety.SoftwareSystems-BusyBox-MemSafety
      - no-overflow.SoftwareSystems-BusyBox-NoOverflows
      - unreach-call.SoftwareSystems-DeviceDriversLinux64-ReachSafety
      - unreach-call.SoftwareSystems-DeviceDriversLinux64Large-ReachSafety
      - valid-memsafety.SoftwareSystems-OpenBSD-MemSafety
      - valid-memsafety.SoftwareSystems-uthash-MemSafety
      - no-overflow.SoftwareSystems-uthash-NoOverflows
      - unreach-call.SoftwareSystems-uthash-ReachSafety
Dirk Beyer's avatar
Dirk Beyer committed
1047
1048
1049
    verifiers:
      - 2ls
      - cbmc
1050
      - coveriteam-verifier-parallel-portfolio
Dirk Beyer's avatar
Dirk Beyer committed
1051
      - cpa-bam-bnb
1052
      - cpa-bam-smg
1053
      - cpachecker
Dirk Beyer's avatar
Dirk Beyer committed
1054
      - divine
1055
      - esbmc-kind
1056
      - goblint