CELL: A compositional verification framework

This paper presents CELL, a comprehensive and extensible framework for compositional verification of concurrent and real-time systems based on commonly used semantic models. For each semantic model, CELL offers three libraries, i.e., compositional verification paradigms, learning algorithms and mode...

Full description

Saved in:
Bibliographic Details
Main Authors: JI, Kun, LIU, Yang, SUN, Jun, DONG, Jin Song, NGUYEN, Truong Khanh
Format: text
Language:English
Published: Institutional Knowledge at Singapore Management University 2013
Subjects:
Online Access:https://ink.library.smu.edu.sg/sis_research/4997
https://ink.library.smu.edu.sg/context/sis_research/article/6000/viewcontent/cell.pdf
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary:This paper presents CELL, a comprehensive and extensible framework for compositional verification of concurrent and real-time systems based on commonly used semantic models. For each semantic model, CELL offers three libraries, i.e., compositional verification paradigms, learning algorithms and model checking methods to support various state-of-the-art compositional verification approaches. With well-defined APIs, the framework could be applied to build customized model checkers. In addition, each library could be used independently for verification and program analysis purposes. We have built three model checkers with CELL. The experimental results show that the performance of these model checkers can offer similar or often better performance compared to the state-of-the-art verification tools.