Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community

Kristin Y. Rozier; Natarajan Shankar; Cesare Tinelli; Moshe Vardi

doi:10.34727/2023/isbn.978-3-85448-060-0_4

Back

Conference proceeding

Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community

Kristin Y. Rozier, Natarajan Shankar, Cesare Tinelli and Moshe Vardi

2023 Formal Methods in Computer-Aided Design (FMCAD), pp.1-1

10/24/2023

DOI: 10.34727/2023/isbn.978-3-85448-060-0_4

Files and links (1)

url

https://doi.org/10.34727/2023/isbn.978-3-85448-060-0_4View

Open Access

Abstract

As model checking becomes more integrated into the standard design and verification process for safety-critical systems, the platforms for model checking research have become more limited. Previous options have become closed-source or industry tools; current research platforms don't have support for expressive specification languages needed for verifying real systems. Our goal is to fill the current gap in model checking research platforms: building a freely-available, open-source, scalable model checking infrastructure that accepts expressive models and efficiently interfaces with the currently-maintained state-of-the-art back-end algorithms to provide an extensible research and verification tool. With extensive involvement from the research community, we have been creating a community resource with a well-documented intermediate representation to enable extensibility, and a web portal, facilitating new modeling languages and back-end algorithmic advances. To add new modeling languages or algorithms, researchers need only to develop a translator to/from the new intermediate language, and will then be able to integrate each advance with the full state-of-the-art in model checking. This tutorial will include an overview of the model checking intermediate language semantics and demonstrations of (provably correct) translators to and from that representation.

Semantics

Computational modeling

Design automation

Extensibility

Industries

Model checking

Tutorials

Details

Title: Subtitle: Developing an Open-Source, State-of-the-Art Symbolic Model-Checking Framework for the Model-Checking Research Community
Creators: Kristin Y. Rozier - Iowa State University
Natarajan Shankar - Menlo School
Cesare Tinelli - University of Iowa,Iowa City,IA,USA
Moshe Vardi - Rice University
Resource Type: Conference proceeding
Publication Details: 2023 Formal Methods in Computer-Aided Design (FMCAD), pp.1-1
DOI: 10.34727/2023/isbn.978-3-85448-060-0_4
eISSN: 2708-7824
Publisher: FMCAD Association and individual authors
Language: English
Date published: 10/24/2023
Academic Unit: Computer Science
Record Identifier: 9984528102002771

Metrics

84 Record Views