Service interruption on Monday 11 July from 12:30 to 13:00: all the sites of the CCSD (HAL, Epiciences, SciencesConf, AureHAL) will be inaccessible (network hardware connection).
Skip to Main content Skip to Navigation
Conference papers

Model Checking of Concurrent Algorithms: From Java to C

Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [23 references]  Display  Hide  Download
Contributor : Hal Ifip Connect in order to contact the contributor
Submitted on : Thursday, August 7, 2014 - 11:15:08 AM
Last modification on : Monday, May 17, 2021 - 12:00:04 PM
Long-term archiving on: : Wednesday, November 26, 2014 - 1:06:44 AM


Files produced by the author(s)


Distributed under a Creative Commons Attribution 4.0 International License



Cyrille Artho, Masami Hagiya, Watcharin Leungwattanakit, yoshinori Tanabe, Mitsuharu yamamoto. Model Checking of Concurrent Algorithms: From Java to C. 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) , Sep 2010, Brisbane, Australia. pp.90-101, ⟨10.1007/978-3-642-15234-4_10⟩. ⟨hal-01054483⟩



Record views


Files downloads