%0 Conference Proceedings
%T Model Checking of Concurrent Algorithms: From Java to C
%+ Research Center for Information Security (RCIS)
%+ The University of Tokyo (UTokyo)
%+ National Institute of Informatics (NII)
%+ Chiba University
%A Artho, Cyrille
%A Hagiya, Masami
%A Leungwattanakit, Watcharin
%A Tanabe, Yoshinori
%A Yamamoto, Mitsuharu
%< avec comité de lecture
%( IFIP Advances in Information and Communication Technology
%B 7th IFIP TC 10 Working Conference on Distributed, Parallel and Biologically Inspired Systems (DIPES) / 3rd IFIP TC 10 International Conference on Biologically-Inspired Collaborative Computing (BICC) / Held as Part of World Computer Congress (WCC)
%C Brisbane, Australia
%Y Mike Hinchey; Bernd Kleinjohann; Lisa Kleinjohann; Peter A. Lindsay; Franz J. Rammig; Jon Timmis; Marilyn Wolf
%I Springer
%3 Distributed, Parallel and Biologically Inspired Systems
%V AICT-329
%P 90-101
%8 2010-09-20
%D 2010
%R 10.1007/978-3-642-15234-4_10
%Z Computer Science [cs]/Digital Libraries [cs.DL]Conference papers
%X Concurrent software is difficult to verify. Because the thread schedule is not controlled by the application, testing may miss defects that occur under specific thread schedules. This problem gave rise to software model checking, where the outcome of all possible thread schedules is analyzed. Among existing software model checkers for multi-threaded programs, Java PathFinder for Java bytecode is probably the most flexible one. We argue that compared to C programs, the virtual machine architecture of Java, combined with the absence of direct low-level memory access, lends itself to software model checking using a virtual machine approach. C model checkers, on the other hand, often use a stateless approach, where it is harder to avoid redundancy in the analysis. Because of this, we found it beneficial to prototype a concurrent algorithm in Java, and use the richer feature set of a Java model checker, before moving our implementation to C. As the thread models are nearly identical, such a transition does not incur high development cost. Our case studies confirm the potential of our approach.
%G English
%2 https://inria.hal.science/hal-01054483/document
%2 https://inria.hal.science/hal-01054483/file/final_008.pdf
%L hal-01054483
%U https://inria.hal.science/hal-01054483
%~ IFIP
%~ IFIP-AICT
%~ IFIP-AICT-329
%~ IFIP-TC
%~ IFIP-TC10
%~ IFIP-WCC
%~ IFIP-2010
%~ IFIP-DIPES
%~ IFIP-BICC