Automatic Verification of C and Java']Java Programs: SV-COMP 2019

被引:57
|
作者
Beyer, Dirk [1 ]
机构
[1] Ludwig Maximilians Univ Munchen, Munich, Germany
关键词
BOUNDED MODEL CHECKING; COMPETITION; ABSTRACTION; TERMINATION;
D O I
10.1007/978-3-030-17502-3_9
中图分类号
TP18 [人工智能理论];
学科分类号
081104 ; 0812 ; 0835 ; 1405 ;
摘要
This report describes the 2019 Competition on Software Verification (SV-COMP), the 8th edition of a series of comparative evaluations of fully automatic software verifiers for C programs, and now also for Java programs. The competition provides a snapshot of the current state of the art in the area, and has a strong focus on replicability of its results. The repository of benchmark verification tasks now supports a new, more flexible format for task definitions (based on YAML), which was a precondition for conveniently benchmarking Java programs in the same controlled competition setting that was successfully applied in the previous years. The competition was based on 10 522 verification tasks for C programs and 368 verification tasks for Java programs. Each verification task consisted of a program and a property (reachability, memory safety, overflows, termination). SV-COMP 2019 had 31 participating verification systems from 14 countries.
引用
收藏
页码:133 / 155
页数:23
相关论文
共 50 条
  • [1] Java']Java Pathfinder at SV-COMP 2019 (Competition Contribution)
    Artho, Cyrille
    Visser, Willem
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, 2019, 11429 : 224 - 228
  • [2] Java']Java Ranger at SV-COMP 2020 (Competition Contribution)
    Sharma, Vaibhav
    Hussein, Soha
    Whalen, Michael W.
    McCamant, Stephen
    Visser, Willem
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 393 - 397
  • [3] Advances in Automatic Software Verification: SV-COMP 2020
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2020, 2020, 12079 : 347 - 367
  • [4] Competition on Software Verification (SV-COMP)
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2012, 2012, 7214 : 504 - 524
  • [5] Automatic verification of Java']Java programs with dynamic frames
    Smans, Jan
    Jacobs, Bart
    Piessens, Frank
    Schulte, Wolfram
    [J]. FORMAL ASPECTS OF COMPUTING, 2010, 22 (3-4) : 423 - 457
  • [6] Progress on Software Verification: SV-COMP 2022
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2022, PT II, 2022, 13244 : 375 - 402
  • [7] Competition on Software Verification and Witness Validation: SV-COMP 2023
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT II, TACAS 2023, 2023, 13994 : 495 - 522
  • [8] Second Competition on Software Verification (Summary of SV-COMP 2013)
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 594 - 609
  • [9] Verification of Java']Java programs with generics
    Stenzel, Kurt
    Grandy, Holger
    Reif, Wolfgang
    [J]. ALGEBRAIC METHODOLOGY AND SOFTWARE TECHNOLOGY, PROCEEDINGS, 2008, 5140 : 315 - 329
  • [10] Software Verification with Validation of Results (Report on SV-COMP 2017)
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2017, PT II, 2017, 10206 : 331 - 349