Abstract
How do you prove the correctness of multi-threaded code? This question has been asked since at least the mid-sixties, and it has inspired researchers ever since. Many approaches have been tried, based on mathematical theories, the use of annotations, or the construction of abstractions. An ideal solution would be a tool that one can point at an arbitrary piece of concurrent code, and that can resolve correctness queries in real-time. We describe one possible method for achieving this capability with a logic model checker.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bloom, B.H.: Spacetime trade-offs in hash coding with allowable errors. Comm. ACM 13(7), 422–426 (1970)
Holzmann, G.J.: On limits and possibilities of automated protocol analysis. In: Rudin, H., West, C. (eds.) Proc. 6th Int. Conf. on Protocol Specification Testing and Verification, INWG IFIP, Zurich Switzerland (June 1987)
Holzmann, G.J., Smith, M.H.: Software model checking – extracting verification models from source code. In: Formal Methods for Protocol Engineering and Distributed Systems, pp. 481–497. Kluwer Academic Publ. (October 1999), also in: Software Testing Verification and Reliability 11(2), 65–79 (June 2001)
Holzmann, G.J.: Logic Verification of ANSI-C Code with Spin. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol. 1885, pp. 131–147. Springer, Heidelberg (2000)
Holzmann, G.J., Smith, M.H.: Automating software feature verification. Bell Labs Technical Journal 5(2), 72–87 (2000)
Holzmann, G.J.: The Spin Model Checker: Primer and Reference Manual. Addison-Wesley (2004)
Holzmann, G.J., Florian, M.: Model checking with bounded context switching. Formal Aspects of Computing 23(3), 365–389 (2011)
Holzmann, G.J., Joshi, R., Groce, A.: Swarm verification techniques. IEEE Trans. on Software Eng. 37(6), 845–857 (2011)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Holzmann, G.J. (2013). Proving Properties of Concurrent Programs. In: Bartocci, E., Ramakrishnan, C.R. (eds) Model Checking Software. SPIN 2013. Lecture Notes in Computer Science, vol 7976. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39176-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-39176-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39175-0
Online ISBN: 978-3-642-39176-7
eBook Packages: Computer ScienceComputer Science (R0)