Software Architecture of Modern Model Checkers

Fabrice Kordon, Michael Leuschel, Jaco van de Pol, Yann Thierry-Mieg

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

2 Citations (Scopus)

Abstract

Automated formal verification using model checking is a mature field with many tools available. We summarize the recent trends in the design and architecture of model checking tools. An important design goal of modern model checkers is to support many input languages (front-end) and many verification strategies (back-end), and to allow arbitrary combinations of them. This widens the applicability of new verification algorithms, avoids duplicate implementation of the analysis techniques, improves quality of the tools, and eases use of verification for a newly introduced high-level specification, such as a domain specific language.
Original languageEnglish
Title of host publicationComputing and Software Science
Subtitle of host publicationState of the Art and Perspectives
EditorsBernhard Steffen, Gerhard Woeginger
Place of PublicationCham
PublisherSpringer
Pages393-419
Number of pages27
ISBN (Electronic)978-3-319-91908-9
ISBN (Print)978-3-319-91907-2
DOIs
Publication statusPublished - 2019

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume10000
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349
NameTheoretical Computer Science and General Issues
PublisherSpringer

Fingerprint Dive into the research topics of 'Software Architecture of Modern Model Checkers'. Together they form a unique fingerprint.

Cite this