Combining syntactic and semantic encoding for LTL bounded model checking

Wanwei Liu; Xiaoguang Mao; Geguang Pu; Rui Wang

doi:10.1109/TASE.2014.13

Combining syntactic and semantic encoding for LTL bounded model checking

Wanwei Liu
, Xiaoguang Mao
, Geguang Pu
, Rui Wang

Software Engineering Institute

National University of Defense Technology

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

2 Scopus citations

Abstract

Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with "next" operator and "until" operator in the specification. The proposed encoding could be implemented in an "on-the-fly" manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.

Original language	English
Title of host publication	Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	82-89
Number of pages	8
ISBN (Electronic)	9781479950294
DOIs	https://doi.org/10.1109/TASE.2014.13
State	Published - 4 Dec 2014
Event	8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014 - Changsha, China Duration: 1 Sep 2014 → 3 Sep 2014

Publication series

Name	Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014

Conference

Conference	8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014
Country/Territory	China
City	Changsha
Period	1/09/14 → 3/09/14

Access to Document

10.1109/TASE.2014.13

Cite this

Liu, W., Mao, X., Pu, G., & Wang, R. (2014). Combining syntactic and semantic encoding for LTL bounded model checking. In Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014 (pp. 82-89). Article 6976572 (Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/TASE.2014.13

Liu, Wanwei ; Mao, Xiaoguang ; Pu, Geguang et al. / Combining syntactic and semantic encoding for LTL bounded model checking. Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014. Institute of Electrical and Electronics Engineers Inc., 2014. pp. 82-89 (Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014).

@inproceedings{2e98761fad044ece9fbf1a2d56cb4a3a,

title = "Combining syntactic and semantic encoding for LTL bounded model checking",

abstract = "Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with {"}next{"} operator and {"}until{"} operator in the specification. The proposed encoding could be implemented in an {"}on-the-fly{"} manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.",

author = "Wanwei Liu and Xiaoguang Mao and Geguang Pu and Rui Wang",

note = "Publisher Copyright: Copyright {\textcopyright} 2014 by The Institute of Electrical and Electronics Engineers, Inc.; 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014 ; Conference date: 01-09-2014 Through 03-09-2014",

year = "2014",

month = dec,

day = "4",

doi = "10.1109/TASE.2014.13",

language = "英语",

series = "Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "82--89",

booktitle = "Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014",

address = "美国",

}

Liu, W, Mao, X, Pu, G & Wang, R 2014, Combining syntactic and semantic encoding for LTL bounded model checking. in Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014., 6976572, Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Institute of Electrical and Electronics Engineers Inc., pp. 82-89, 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014, Changsha, China, 1/09/14. https://doi.org/10.1109/TASE.2014.13

Combining syntactic and semantic encoding for LTL bounded model checking. / Liu, Wanwei; Mao, Xiaoguang; Pu, Geguang et al.
Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014. Institute of Electrical and Electronics Engineers Inc., 2014. p. 82-89 6976572 (Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Combining syntactic and semantic encoding for LTL bounded model checking

AU - Liu, Wanwei

AU - Mao, Xiaoguang

AU - Pu, Geguang

AU - Wang, Rui

PY - 2014/12/4

Y1 - 2014/12/4

N2 - Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with "next" operator and "until" operator in the specification. The proposed encoding could be implemented in an "on-the-fly" manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.

AB - Bounded model checking (BMC, for short) is a successful application of SAT technique in model checking. In a broad sense, BMC encoding approaches could be categorised into the syntactic fashion and semantic fashion. In this paper, we present a new BMC encoding approach specially tailored for LTL model checking. The key observation is that syntactic encoding and semantic encoding respectively have the superiority in dealing with "next" operator and "until" operator in the specification. The proposed encoding could be implemented in an "on-the-fly" manner, and finally results in a linear scale blow-up. To justify it, the approach is experimentally evaluated by comparing with some of the best known existing encodings.

UR - https://www.scopus.com/pages/publications/84920409373

U2 - 10.1109/TASE.2014.13

DO - 10.1109/TASE.2014.13

M3 - 会议稿件

AN - SCOPUS:84920409373

T3 - Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014

SP - 82

EP - 89

BT - Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 8th International Symposium on Theoretical Aspects of Software Engineering, TASE 2014

Y2 - 1 September 2014 through 3 September 2014

ER -

Liu W, Mao X, Pu G, Wang R. Combining syntactic and semantic encoding for LTL bounded model checking. In Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014. Institute of Electrical and Electronics Engineers Inc. 2014. p. 82-89. 6976572. (Proceedings - 2014 International Symposium on Theoretical Aspects of Software Engineering, TASE 2014). doi: 10.1109/TASE.2014.13

Combining syntactic and semantic encoding for LTL bounded model checking

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this