DIVINE: Explicit-State LTL Model Checker (Competition Contribution)

被引：5
|
作者：
Still, Vladimir [1 ]
Rockai, Petr [1 ]
Barnat, Jiri [1 ]
机构：
[1] Masaryk Univ, Fac Informat, Brno, Czech Republic
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS (TACAS 2016) | 2016年 / 9636卷
关键词：
D O I：
10.1007/978-3-662-49674-9_60
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
DIVINE is an LLVM-based LTL model checker that follows the standard automata-based approach to explicit-state model checking. It aims at verification of unmodified parallel C & C++ programs without inputs. To achieve this DIVINE employs several reduction techniques combined with high-performance parallel and distributed computing.
引用
收藏
页码：920 / 922
页数：3
相关论文
共 50 条
  • [1] On the Scalability of the GPUEXPLORE Explicit-State Model Checker
    Cassee, Nathan
    Neele, Thomas
    Wijs, Anton
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2017, (263): : 38 - 52
  • [2] CPACHECKER with Sequential Combination of Explicit-State Analysis and Predicate Analysis (Competition Contribution)
    Wendler, Philipp
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, TACAS 2013, 2013, 7795 : 613 - 615
  • [3] DiVinE Multi-Core - A Parallel LTL Model-Checker
    Barnat, Jiri
    Brim, Lubos
    Rockai, Petr
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2008, 5311 : 234 - 239
  • [4] AutoHyper: Explicit-State Model Checking for HyperLTL
    Beutner, Raven
    Finkbeiner, Bernd
    [J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PT I, TACAS 2023, 2023, 13993 : 145 - 163
  • [5] Quo Vadis Explicit-State Model Checking
    Sankowski, Piotr
    [J]. SOFSEM 2015: THEORY AND PRACTICE OF COMPUTER SCIENCE, 2015, 8939 : 46 - 57
  • [6] An FPGA Implementation of Explicit-State Model Checking
    Fuess, Mary Ellen
    Leeser, Miriam
    Leonard, Tim
    [J]. PROCEEDINGS OF THE SIXTEENTH IEEE SYMPOSIUM ON FIELD-PROGRAMMABLE CUSTOM COMPUTING MACHINES, 2008, : 119 - +
  • [7] Directed explicit-state model checking in the validation of communication protocols
    Stefan Edelkamp
    Stefan Leue
    Alberto Lluch-Lafuente
    [J]. International Journal on Software Tools for Technology Transfer, 2004, 5 (2-3) : 247 - 267
  • [8] A Progress Measure for Explicit-State Probabilistic Model-Checkers
    Zhang, Xin
    van Breugel, Franck
    [J]. AUTOMATA, LANGUAGES AND PROGRAMMING, ICALP, PT II, 2011, 6756 : 283 - 294
  • [9] Exploiting heap symmetries in explicit-state model checking of software
    Iosif, R
    [J]. 16TH ANNUAL INTERNATIONAL CONFERENCE ON AUTOMATED SOFTWARE ENGINEERING (ASE 2001), PROCEEDINGS, 2001, : 254 - 261
  • [10] GPUexplore 2.0: Unleashing GPU Explicit-State Model Checking
    Wijs, Anton
    Neele, Thomas
    Bosnacki, Dragan
    [J]. FM 2016: FORMAL METHODS, 2016, 9995 : 694 - 701
12345