Harnessing SMT-based bounded model checking through stateless explicit-state exploration

Weiqiang Kong, Leyuan Liu, Takahiro Ando, Hirokazu Yatsu, Hisazumi Kenji, Akira Fukuda

Research output: Chapter in Book/Report/Conference proceedingConference contribution

2 Citations (Scopus)

Abstract

We propose a hybrid approach to improving the verification performance of SMT-based bounded model checking for LTL properties. In this approach, stateless explicitstate exploration is utilized to traverse, under the constraints of bounded context switches, the state space of a system design and memorize legal execution paths. These paths are classified according to certain predicates into path clusters, which are then encoded into propositional formulas representing, together with the encoded formula for an LTL property, independent BMC instances. Such BMC instances are solved with SMT solvers running on mutilcores in parallel. Once a counterexample is found for one of the instances, the entire model checking terminates. This hybrid checking procedure progresses in an incremental fashion until either a counterexample is found or the user-specified bound is reached. We have implemented this proposed hybrid approach in a tool called Garakabu2 with CVC4 as its backend solver. The experimental results show that Garakabu2 often outperforms the state-of-the-art pure BMC methods implemented in SAL infinite bounded model checker for both safety and liveness properties.

Original languageEnglish
Title of host publicationAPSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference
EditorsPornsiri Muenchaisri, Gregg Rothermel
PublisherIEEE Computer Society
Pages355-362
Number of pages8
Volume1
ISBN (Electronic)9781479921430
ISBN (Print)9780769549224
DOIs
Publication statusPublished - Jan 1 2013
Event20th Asia-Pacific Software Engineering Conference, APSEC 2013 - Bangkok, Thailand
Duration: Dec 2 2013Dec 5 2013

Other

Other20th Asia-Pacific Software Engineering Conference, APSEC 2013
CountryThailand
CityBangkok
Period12/2/1312/5/13

Fingerprint

Surface mount technology
Model checking
Systems analysis
Switches

All Science Journal Classification (ASJC) codes

  • Software

Cite this

Kong, W., Liu, L., Ando, T., Yatsu, H., Kenji, H., & Fukuda, A. (2013). Harnessing SMT-based bounded model checking through stateless explicit-state exploration. In P. Muenchaisri, & G. Rothermel (Eds.), APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference (Vol. 1, pp. 355-362). [6805426] IEEE Computer Society. https://doi.org/10.1109/APSEC.2013.55

Harnessing SMT-based bounded model checking through stateless explicit-state exploration. / Kong, Weiqiang; Liu, Leyuan; Ando, Takahiro; Yatsu, Hirokazu; Kenji, Hisazumi; Fukuda, Akira.

APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. ed. / Pornsiri Muenchaisri; Gregg Rothermel. Vol. 1 IEEE Computer Society, 2013. p. 355-362 6805426.

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Kong, W, Liu, L, Ando, T, Yatsu, H, Kenji, H & Fukuda, A 2013, Harnessing SMT-based bounded model checking through stateless explicit-state exploration. in P Muenchaisri & G Rothermel (eds), APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. vol. 1, 6805426, IEEE Computer Society, pp. 355-362, 20th Asia-Pacific Software Engineering Conference, APSEC 2013, Bangkok, Thailand, 12/2/13. https://doi.org/10.1109/APSEC.2013.55
Kong W, Liu L, Ando T, Yatsu H, Kenji H, Fukuda A. Harnessing SMT-based bounded model checking through stateless explicit-state exploration. In Muenchaisri P, Rothermel G, editors, APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. Vol. 1. IEEE Computer Society. 2013. p. 355-362. 6805426 https://doi.org/10.1109/APSEC.2013.55
Kong, Weiqiang ; Liu, Leyuan ; Ando, Takahiro ; Yatsu, Hirokazu ; Kenji, Hisazumi ; Fukuda, Akira. / Harnessing SMT-based bounded model checking through stateless explicit-state exploration. APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference. editor / Pornsiri Muenchaisri ; Gregg Rothermel. Vol. 1 IEEE Computer Society, 2013. pp. 355-362
@inproceedings{d9d52334ed324e4c8099fd27be7646c3,
title = "Harnessing SMT-based bounded model checking through stateless explicit-state exploration",
abstract = "We propose a hybrid approach to improving the verification performance of SMT-based bounded model checking for LTL properties. In this approach, stateless explicitstate exploration is utilized to traverse, under the constraints of bounded context switches, the state space of a system design and memorize legal execution paths. These paths are classified according to certain predicates into path clusters, which are then encoded into propositional formulas representing, together with the encoded formula for an LTL property, independent BMC instances. Such BMC instances are solved with SMT solvers running on mutilcores in parallel. Once a counterexample is found for one of the instances, the entire model checking terminates. This hybrid checking procedure progresses in an incremental fashion until either a counterexample is found or the user-specified bound is reached. We have implemented this proposed hybrid approach in a tool called Garakabu2 with CVC4 as its backend solver. The experimental results show that Garakabu2 often outperforms the state-of-the-art pure BMC methods implemented in SAL infinite bounded model checker for both safety and liveness properties.",
author = "Weiqiang Kong and Leyuan Liu and Takahiro Ando and Hirokazu Yatsu and Hisazumi Kenji and Akira Fukuda",
year = "2013",
month = "1",
day = "1",
doi = "10.1109/APSEC.2013.55",
language = "English",
isbn = "9780769549224",
volume = "1",
pages = "355--362",
editor = "Pornsiri Muenchaisri and Gregg Rothermel",
booktitle = "APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference",
publisher = "IEEE Computer Society",
address = "United States",

}

TY - GEN

T1 - Harnessing SMT-based bounded model checking through stateless explicit-state exploration

AU - Kong, Weiqiang

AU - Liu, Leyuan

AU - Ando, Takahiro

AU - Yatsu, Hirokazu

AU - Kenji, Hisazumi

AU - Fukuda, Akira

PY - 2013/1/1

Y1 - 2013/1/1

N2 - We propose a hybrid approach to improving the verification performance of SMT-based bounded model checking for LTL properties. In this approach, stateless explicitstate exploration is utilized to traverse, under the constraints of bounded context switches, the state space of a system design and memorize legal execution paths. These paths are classified according to certain predicates into path clusters, which are then encoded into propositional formulas representing, together with the encoded formula for an LTL property, independent BMC instances. Such BMC instances are solved with SMT solvers running on mutilcores in parallel. Once a counterexample is found for one of the instances, the entire model checking terminates. This hybrid checking procedure progresses in an incremental fashion until either a counterexample is found or the user-specified bound is reached. We have implemented this proposed hybrid approach in a tool called Garakabu2 with CVC4 as its backend solver. The experimental results show that Garakabu2 often outperforms the state-of-the-art pure BMC methods implemented in SAL infinite bounded model checker for both safety and liveness properties.

AB - We propose a hybrid approach to improving the verification performance of SMT-based bounded model checking for LTL properties. In this approach, stateless explicitstate exploration is utilized to traverse, under the constraints of bounded context switches, the state space of a system design and memorize legal execution paths. These paths are classified according to certain predicates into path clusters, which are then encoded into propositional formulas representing, together with the encoded formula for an LTL property, independent BMC instances. Such BMC instances are solved with SMT solvers running on mutilcores in parallel. Once a counterexample is found for one of the instances, the entire model checking terminates. This hybrid checking procedure progresses in an incremental fashion until either a counterexample is found or the user-specified bound is reached. We have implemented this proposed hybrid approach in a tool called Garakabu2 with CVC4 as its backend solver. The experimental results show that Garakabu2 often outperforms the state-of-the-art pure BMC methods implemented in SAL infinite bounded model checker for both safety and liveness properties.

UR - http://www.scopus.com/inward/record.url?scp=84936853944&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84936853944&partnerID=8YFLogxK

U2 - 10.1109/APSEC.2013.55

DO - 10.1109/APSEC.2013.55

M3 - Conference contribution

AN - SCOPUS:84936853944

SN - 9780769549224

VL - 1

SP - 355

EP - 362

BT - APSEC 2013 - Proceedings of the 20th Asia-Pacific Software Engineering Conference

A2 - Muenchaisri, Pornsiri

A2 - Rothermel, Gregg

PB - IEEE Computer Society

ER -