Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
10-2013
Abstract
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.
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18
First Page
474
Last Page
477
ISBN
9783319024431
Identifier
10.1007/978-3-319-02444-8_38
Publisher
Springer Link
City or Country
Hanoi, Vietnam
Citation
JI, Kun; LIU, Yang; SUN, Jun; SUN, Jun; DONG, Jin Song; and NGUYEN, Truong Khanh.
CELL: A compositional verification framework. (2013). Proceedings of the 11th International Symposium, ATVA 2013, Hanoi, Vietnam, October 15-18. 474-477.
Available at: https://ink.library.smu.edu.sg/sis_research/4997
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-319-02444-8_38