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 条
  • [21] Software Verification: 10th Comparative Evaluation (SV-COMP 2021)
    Beyer, Dirk
    [J]. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2021, 12652 LNCS : 401 - 422
  • [22] Verification of Java']Java Programs with Interacting Analysis Plugins
    Charlton, Nathaniel
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2006, 145 : 131 - 150
  • [23] Specification and Runtime Verification of Java']Java Card Programs
    da Costa, Umberto Souza
    Moreira, Anamaria Martins
    Musicante, Martin A.
    Souza Neto, Placido A.
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2009, 240 : 61 - 78
  • [24] Towards the automated verification of multithreaded Java']Java programs
    Delzanno, G
    Raskin, JF
    Van Begin, L
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANAYLSIS OF SYSTEMS, PROCEEDINGS, 2002, 2280 : 173 - 187
  • [25] Verification of Java programs in Coq
    Department of Computer Science, Royal Holloway University of London, Surrey, United Kingdom
    [J]. Comput. Sci. Electron. Eng. Conf., CEEC,
  • [26] A step toward automatic distribution of Java']Java programs
    Attali, I
    Caromel, D
    Guider, R
    [J]. FORMAL METHODS FOR OPEN OBJECT-BASED DISTRIBUTED SYSTEMS IV, 2000, 49 : 141 - 161
  • [27] On-Device Control Flow Verification for Java']Java Programs
    Fontaine, Arnaud
    Hym, Samuel
    Simplot-Ryl, Isabelle
    [J]. ENGINEERING SECURE SOFTWARE AND SYSTEMS, 2011, 6542 : 43 - 57
  • [28] Formal verification of protocol properties of sequential Java']Java programs
    Jin, Ying
    [J]. COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS, 2007, : 475 - 482
  • [29] Verification of Snapshot Isolation in Transactional Memory Java']Java Programs
    Dias, Ricardo J.
    Distefano, Dino
    Seco, Joao Costa
    Lourenco, Joao M.
    [J]. ECOOP 2012 - OBJECT-ORIENTED PROGRAMMING, 2012, 7313 : 640 - 664
  • [30] A Framework for the Cryptographic Verification of Java']Java-like Programs
    Kuesters, Ralf
    Truderung, Tomasz
    Graf, Juergen
    [J]. 2012 IEEE 25TH COMPUTER SECURITY FOUNDATIONS SYMPOSIUM (CSF), 2012, : 198 - 212