Abstract
With the growth of multi-core processing and concurrent programming in modern computing systems, there is a great need to develop effective verification techniques for concurrent programs. Static analysis techniques have been shown effective for finding data races, but suffer from a general problem of too many false alarms. Dynamic techniques like testing have also shown promise, but provide limited coverage over the state space including all possible thread interleavings. Model checking alone cannot scale. However, it works better in combination with these techniques, with the potential of finding real error traces on one hand and better coverage on the other. In this talk, I will describe our recent advances in concurrent dataflow analysis, symbolic model checking with partial order reduction, and dynamic techniques for verifying concurrent programs. These techniques have been implemented in a unified verification platform, currently targeted at multi-threaded C programs. I will also report on our experiences on some challenging examples from the public domain and the industry.
Chapter PDF
Similar content being viewed by others
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gupta, A. (2008). Model Checking Concurrent Programs. In: Jones, N.D., Müller-Olm, M. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2009. Lecture Notes in Computer Science, vol 5403. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-93900-9_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-93900-9_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-93899-6
Online ISBN: 978-3-540-93900-9
eBook Packages: Computer ScienceComputer Science (R0)