Concurrent Bounded Model Checking (2024)

Видання: ACM SIGSOFT Software Engineering Notes, 2015, №1, с.1-5

Видавець: Association for Computing Machinery (ACM)

Автори: Quoc-Sang Phan, Pasquale Malacaria, Corina S. Pǎsǎreanu

Анотація

We introduce a methodology, based on symbolic execution, for Concurrent Bounded Model Checking. In our approach, we translate a program into a formula in a disjunctive form. This design enables concurrent verification, with a main thread running symbolic execution, without any constraint solving, to build subformulas, and a set of worker threads running a decision procedure for satisfiability checks. We have implemented this methodology in a tool called JCBMC, the first bounded model checker for Java. JCBMC is built as an extension of Java Pathfinder, an open-source verification platform developed by NASA. JCBMC uses Symbolic PathFinder (SPF) for the symbolic execution, Z3 as the solver and implements concurrency with multi-threading. For evaluation, we compare JCBMC against SPF and the Bounded Model Checker CBMC. The results of the experiments show that we can achieve significant advantages of performance over these two tools.

Список літератури

Benchmarks of loops in the Software Verification 2014 competition 2014. https://svn.sosy-lab.org/software/sv benchmarks/tags/svcomp14/loops/. Benchmarks of loops in the Software Verification 2014 competition 2014. https://svn.sosy-lab.org/software/sv benchmarks/tags/svcomp14/loops/.
Java PathFinder. http://babelfish.arc.nasa.gov/trac/jpf/. Java PathFinder. http://babelfish.arc.nasa.gov/trac/jpf/.
Z3. http://z3.codeplex.com/. Z3. http://z3.codeplex.com/.
Erika Ábrahám , Tobias Schubert , Bernd Becker , Martin Fränzle , and Christian Herde . Parallel sat solving in bounded model checking . FMICS'06/PDMC'06 , pages 301 -- 315 . Erika Ábrahám, Tobias Schubert, Bernd Becker, Martin Fränzle, and Christian Herde. Parallel sat solving in bounded model checking. FMICS'06/PDMC'06, pages 301--315.
Cristian Cadar , Daniel Dunbar , and Dawson Engler . Klee : unassisted and automatic generation of high-coverage tests for complex systems programs . OSDI'08 , pages 209 -- 224 . Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. OSDI'08, pages 209--224.
Patrice Godefroid , Michael Y. Levin , and David A. Molnar . Automated whitebox fuzz testing . In NDSS , 2008 . Patrice Godefroid, Michael Y. Levin, and David A. Molnar. Automated whitebox fuzz testing. In NDSS, 2008.
Elsa L. Gunter and Doron Peled. Unit checking: Symbolic model checking for a unit of code . In Nachum Dershowitz editor Verification : Theory and Practice Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday volume 2772 of Lecture Notes in Computer Science pages 548 -- 567 . Springer 2003 . Elsa L. Gunter and Doron Peled. Unit checking: Symbolic model checking for a unit of code. In Nachum Dershowitz editor Verification: Theory and Practice Essays Dedicated to Zohar Manna on the Occasion of His 64th Birthday volume 2772 of Lecture Notes in Computer Science pages 548--567. Springer 2003.
https://doi.org/10.1007/978-3-540-39910-0_24
Temesghen Kahsai and Cesare Tinelli . Pkind: A parallel k-induction based model checker . In Jiri Barnat and Keijo Heljanko editors PDMC volume 72 of EPTCS pages 55 -- 62 2011 . Temesghen Kahsai and Cesare Tinelli. Pkind: A parallel k-induction based model checker. In Jiri Barnat and Keijo Heljanko editors PDMC volume 72 of EPTCS pages 55--62 2011.
https://doi.org/10.4204/EPTCS.72.6
Andrew King . Distributed parallel symbolic execution . In Master Thesis , Kansas State University , 2009 . Andrew King. Distributed parallel symbolic execution. In Master Thesis, Kansas State University, 2009.
Marta Z. Kwiatkowska , Alessio Lomuscio , and Hongyang Qu . Parallel model checking for temporal epistemic logic . In ECAI , pages 543 -- 548 , 2010 . Marta Z. Kwiatkowska, Alessio Lomuscio, and Hongyang Qu. Parallel model checking for temporal epistemic logic. In ECAI, pages 543--548, 2010.
Pradeep K. Nalla J. Weiss JÃijrgen Ruf Thomas Kropf and Wolfgang Rosenstiel. Parallel bounded property checking with symc. Pradeep K. Nalla J. Weiss JÃijrgen Ruf Thomas Kropf and Wolfgang Rosenstiel. Parallel bounded property checking with symc.
Robert Palmer and Ganesh Gopalakrishnan . Partial order reduction assisted parallel modelchecking (full version. Technical report , PDMC'2002 , 2002 . Robert Palmer and Ganesh Gopalakrishnan. Partial order reduction assisted parallel modelchecking (full version. Technical report, PDMC'2002, 2002.
Quoc-Sang Phan . Symbolic execution as dpll modulo theories . In 2014 Imperial College Computing Student Workshop , volume 43 of OpenAccess Series in Informatics (OASIcs), pages 58--65, Dagstuhl, Germany , 2014 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik. Quoc-Sang Phan. Symbolic execution as dpll modulo theories. In 2014 Imperial College Computing Student Workshop, volume 43 of OpenAccess Series in Informatics (OASIcs), pages 58--65, Dagstuhl, Germany, 2014. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik.
J.H. Siddiqui and S Khurshid . Parsym : Parallel symbolic execution . In ICSTE , volume 1 , pages V1 -- 405 --V1--409, 2010 . J.H. Siddiqui and S Khurshid. Parsym: Parallel symbolic execution. In ICSTE, volume 1, pages V1--405--V1--409, 2010.
Ulrich Stern and David L. Dill . Parallelizing the murphi verifier . CAV '97 , pages 256 -- 278 , London, UK, UK , 1997 . Springer-Verlag. Ulrich Stern and David L. Dill. Parallelizing the murphi verifier. CAV '97, pages 256--278, London, UK, UK, 1997. Springer-Verlag.

Публікації, які цитують цю публікацію

Extending DIVINE with Symbolic Verification Using SMT

Henrich Lauko, Vladimír Štill, Petr Ročkai, Jiří Barnat

https://doi.org/10.1007/978-3-030-17502-3_14 · Повний текст

2019, Tools and Algorithms for the Construction and Analysis of Systems Lecture Notes in Computer Science, с.204-208

Кількість цитувань	7
Кількість джерел у списку літератури:	15
Видання індексується в Scopus	Ні
Видання індексується в Web of Science	Ні