Concurrent Bounded Model Checking (2024)

Table of Contents

Анотація Список літератури Публікації, які цитують цю публікацію FAQs References

Видання: 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

FAQs

What is the difference between model checking and bounded model checking? ›

In contrast to unbounded model checking, BMC aims at the falsification of safety properties, instead of verification. Basically speaking, BMC searches for counter- examples by unrolling the transition relation of the system model finitely often, hence the term “bounded”.

Read On ›

What are the limitations of model checking? ›

It is particularly useful in artificial intelligence for verifying the correctness of proposed solutions. Some limitations of model checking include the state space explosion problem and temporal logic challenges.

Discover More ›

What is model checking in formal verification? ›

– Model checking is an algorithmic approach to. analysis of finite-state systems. – Model checking has been originally developed for. analysis of hardware designs and communication. protocols.

Get More Info ›

What is the difference between model checking and symbolic execution? ›

The model checker will then make sure that the specification always holds in that system. In symbolic execution you only provide your program and the symbolic execution engine will examine all the feasible paths to generate test inputs or check assertions. A simple example of their difference: concurrency.

Is model checking the same as deductive verification? ›

Deductive verification is a time-consuming process that can be performed only by experts who are educated to logical reasoning. Consequently, it is applied primarily to high sensitive systems such as security protocols. Model checking is a technique for verifying finite state concurrent systems.

Read On ›

What are the advantages of model checking? ›

In contrast to theorem proving, model checking is completely automatic and fast, frequently producing an answer in a matter of minutes. It can be used to check partial specifications and can provide useful information about correctness even if the system has not been completely specified.

Find Out More ›

What are 3 common limitations of models? ›

Limitations of models

They are simplified versions.
They can be interrupted in many different ways.
They do not always cover everything in detail and can miss vital details.
Models are approximations.

Strengths & Limitations of Models - Science: KS3 - Seneca

Seneca

https://senecalearning.com

Seneca

https://senecalearning.com

What is the difference between model checking and testing? ›

What is the difference between model checking and testing? Model Checking: A formal verification technique that systematically explores the states of a system model to verify properties and detect errors. Testing: Involves executing a system or component with various inputs to observe its behavior and identify defects.

What are the 4 types of verification? ›

ANSWER. The four fundamental methods of verification are Inspection, Demonstration, Test, and Analysis. The four methods are somewhat hierarchical in nature, as each verifies requirements of a product or system with increasing rigor.

What is the difference between static analysis and model checking? ›

The static analysis simply requires that the code be compiled, while model checking a system requires a carefully crafted environment model. Also, static analysis can cover all paths in the code in a straightforward manner.

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