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 条
  • [81] Hussein S., 2023, LNCS, V13994, P553, DOI [10.1007/978-3-031-30820-8_35, DOI 10.1007/978-3-031-30820-8_35]
  • [82] Inverso O., 2014, LNCS, V8413, P398, DOI [10.1007/978-3-642-54862-8_29, DOI 10.1007/978-3-642-54862-8_29]
  • [83] Bounded Verification of Multi-threaded Programs via Lazy Sequentialization
    Inverso, Omar
    Tomasco, Ermenegildo
    Fischer, Bernd
    La Torre, Salvatore
    Parlato, Gennaro
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 2022, 44 (01):
  • [84] Parallel and Distributed Bounded Model Checking of Multi-threaded Programs
    Inverso, Omar
    Trubiani, Catia
    [J]. PROCEEDINGS OF THE 25TH ACM SIGPLAN SYMPOSIUM ON PRINCIPLES AND PRACTICE OF PARALLEL PROGRAMMING (PPOPP '20), 2020, : 202 - 216
  • [85] Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution (Competition Contribution)
    Jonas, Martin
    Kumor, Kristian
    Novak, Jakub
    Sedlacek, Jindrich
    Trtik, Marek
    Zaoral, Lukas
    Ayaziova, Paulina
    Strejcek, Jan
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, TACAS 2024, 2024, 14572 : 406 - 411
  • [86] Combinations of Reusable Abstract Domains for a Multilingual Static Analyzer
    Journault, Matthieu
    Mine, Antoine
    Monat, Raphael
    Ouadjaout, Abdelraouf
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, VSTTE 2019, 2020, 12031 : 1 - 18
  • [87] JayHorn: A Framework for Verifying Java']Java programs
    Kahsai, Temesghen
    Rummer, Philipp
    Sanchez, Huascar
    Schaf, Martin
    [J]. COMPUTER AIDED VERIFICATION, (CAV 2016), PT I, 2016, 9779 : 352 - 358
  • [88] The Static Analyzer Infer in SV-COMP (Competition Contribution)
    Kettl, Matthias
    Lemberger, Thomas
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II, 2022, 13244 : 451 - 456
  • [89] Ultimate GemCutter and the Axes of Generalization (Competition Contribution)
    Klumpp, Dominik
    Dietsch, Daniel
    Heizmann, Matthias
    Schuessele, Frank
    Ebbinghaus, Marcel
    Farzan, Azadeh
    Podelski, Andreas
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II, 2022, 13244 : 479 - 483
  • [90] Kroening Daniel, 2014, INT C TOOLS ALGORITH, P389, DOI [10.1007/978-3-642-54862-8_26, DOI 10.1007/978-3-642-54862-8_26, DOI 10.1007/978-3-642-54862-826]
45678910111213