State of the Art in Software Verification and Witness Validation: SV-COMP 2024

被引:16
作者
Beyer, Dirk [1 ]
机构
[1] Ludwig Maximilians Univ Munchen, Munich, Germany
来源
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, TACAS 2024 | 2024年 / 14572卷
关键词
Formal Verification; Program Analysis; Competition; Software Verification; Verification Tasks; Benchmark; Specification; !text type='Java']Java[!/text] Language; C Language; SV-COMP; SV-Benchmarks; BENCHEXEC; COVERITEAM; BOUNDED MODEL CHECKING; ABSTRACT INTERPRETATION; COMPETITION; PROGRAMS; CPA;
D O I
10.1007/978-3-031-57256-2_15
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
The 13th edition of the Competition on Software Verification (SV-COMP 2024) was the largest competition of its kind so far: A total of 76 tools for verification and witness validation were compared. The competition evaluated 59 verification systems and 17 validation systems from 34 teams from 12 countries. This yields a good overview of the state of the art in tools for software verification. The competition was executed on a benchmark set with 30 300 verification tasks for C programs and 587 verification tasks for Java programs. The specifications again included reachability, memory safety, overflows, and termination. This year was the second time that the competition had an extra competition track on witness validation. We introduced a new witness format 2.0, and a new scoring schema for the validation track. All meta data about the verification and validation tools are available in the FM-Tools repository.
引用
收藏
页码:299 / 329
页数:31
相关论文
共 124 条
  • [1] Gazer-Theta: LLVM-based Verifier Portfolio with BMC/CEGAR (Competition Contribution)
    Adam, Zsofia
    Sallai, Gyula
    Hajdu, Akos
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2021, 2021, 12652 : 433 - 437
  • [2] VeriAbs : Verification by Abstraction and Test Generation
    Afzai, Mohammad
    Asia, A.
    Chauhan, Avriti
    Chimdyalwar, Bharti
    Darke, Priyanka
    Datar, Advaita
    Kumar, Shrawan
    Venkatesh, R.
    [J]. 34TH IEEE/ACM INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2019), 2019, : 1138 - 1141
  • [3] EBF 4.2: Black-Box Cooperative Verification for Concurrent Programs (Competition Contribution)
    Aljaafari, Fatimah
    Shmarov, Fedor
    Manino, Edoardo
    Menezes, Rafael
    Cordeiro, Lucas C.
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023, 2023, 13994 : 541 - 546
  • [4] Analysis of Correct Synchronization of Operating System Components
    Andrianov, P. S.
    [J]. PROGRAMMING AND COMPUTER SOFTWARE, 2020, 46 (08) : 712 - 730
  • [5] Andrianov P, 2021, LECT NOTES COMPUT SC, V12652, P423, DOI 10.1007/978-3-030-72013-1_25
  • [6] CPA-BAM-BnB: Block-Abstraction Memoization and Region-Based Memory Models for Predicate Abstractions
    Andrianov, Pavel
    Friedberger, Karlheinz
    Mandrykin, Mikhail
    Mutilin, Vadim
    Volkov, Anton
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II, 2017, 10206 : 355 - 359
  • [7] Ayaziova P., 2024, P SPIN SPRING
  • [8] WITCH 3: Validation of Violation Witnesses in the Witness Format 2.0. (Competition Contribution)
    Ayaziova, Paulina
    Strejcek, Jan
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, TACAS 2024, 2024, 14572 : 341 - 346
  • [9] SYMBIOTIC-WITCH 2: More Efficient Algorithm and Witness Refutation? (Competition Contribution)
    Ayaziova, Paulina
    Strejcek, Jan
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023, 2023, 13994 : 523 - 528
  • [10] CPACHECKER 2.3 with Strategy Selection (Competition Contribution)
    Baier, Daniel
    Beyer, Dirk
    Chien, Po-Chun
    Jankola, Marek
    Kettl, Matthias
    Lee, Nian-Ze
    Lemberger, Thomas
    Lingsch-Rosenfeld, Marian
    Spiessl, Martin
    Wachowitz, Henrik
    Wendler, Philipp
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, TACAS 2024, 2024, 14572 : 359 - 364