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 条
  • [11] Towards Verification and Testing of Java']Java Programs
    de Melo, Ana C. V.
    Nunes, Paulo R. F.
    Xavier, Kleber S.
    [J]. APPLIED COMPUTING 2008, VOLS 1-3, 2008, : 730 - 734
  • [12] Specification and verification of encapsulation in Java']Java programs
    Roth, A
    [J]. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS, PROCEEDINGS, 2005, 3535 : 195 - 210
  • [13] API Conformance Verification for Java']Java Programs
    Li, Xin
    Hoover, H. James
    Rudnicki, Piotr
    [J]. FORMAL METHODS AND SOFTWARE ENGINEERING, 2010, 6447 : 188 - 203
  • [14] Towards Verification of Java']Java Programs in √erICS
    Zbrzezny, Andrzej
    Wozna, Bozena
    [J]. FUNDAMENTA INFORMATICAE, 2008, 85 (1-4) : 533 - 548
  • [15] An experiment in automatic conversion of legacy Java']Java programs to C#
    El-Ramly, Mohammad
    Eltayeb, Rihab
    Alla, Hisham A.
    [J]. 2006 IEEE INTERNATIONAL CONFERENCE ON COMPUTER SYSTEMS AND APPLICATIONS, VOLS 1-3, 2006, : 1036 - +
  • [16] Automatic verification of Java']Java design patterns
    Blewitt, A
    Bundy, A
    Stark, I
    [J]. 16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 324 - 327
  • [17] State of the Art in Software Verification and Witness Validation: SV-COMP 2024
    Beyer, Dirk
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT III, TACAS 2024, 2024, 14572 : 299 - 329
  • [18] Automatic Error Correction of Java']Java Programs
    Kern, Christian
    Esparza, Javier
    [J]. FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, 2010, 6371 : 67 - 81
  • [19] An automatic method for refactoring Java']Java programs
    Yamazaki, S
    Nagata, M
    [J]. KNOWLEDGE-BASED SOFTWARE ENGINEERING, 2002, 80 : 167 - 172
  • [20] Towards automatic specialization of Java']Java programs
    Schultz, UP
    Lawall, JL
    Consel, C
    Muller, G
    [J]. ECOOP'99 - OBJECT-ORIENTED PROGRAMMING, 1999, 1628 : 367 - 390