Skip to main content
Conference ProceedingsOPEN ACCESS

DIVINE: Explicit-state LTL model checker

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (2016) 9636 920-922
DOI: 10.1007/978-3-662-49674-9_60
8Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

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.

Cite

CITATION STYLE

APA

Štill, V., Ročkai, P., & Barnat, J. (2016). DIVINE: Explicit-state LTL model checker. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9636, pp. 920–922). Springer Verlag. https://doi.org/10.1007/978-3-662-49674-9_60

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free