Abstract
This paper reports on the VerCors tool set for verifying parallel and concurrent software. Its main characteristics are (i) that it can verify programs under different concurrency models, written in high-level programming languages, such as for example in Java, OpenCL and OpenMP; and (ii) that it can reason not only about race freedom and memory safety, but also about functional correctness. VerCors builds on top of existing verification technology, notably the Viper framework, by transforming the verification problem of programs written in a high-level programming language into a verification problem in the intermediate language of Viper. This paper presents three examples that illustrate how VerCors support verifying functional correctness of three different concurrency features: heterogeneous concurrency, kernels using barriers and atomic operations, and compiler directives for parallelisation.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Amighi, A., Darabi, S., Blom, S., Huisman, M.: Specification and verification of atomic operations in GPGPU programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 69–83. Springer, Cham (2015). doi:10.1007/978-3-319-22969-0_5
Amighi, A., Haack, C., Huisman, M., Hurlin, C.: Permission-based separation logic for multithreaded Java programs. LMCS 11(1) (2015)
Betts, A., Chong, N., Donaldson, A., Qadeer, S., Thomson, P.: GPUVerify: a verifier for GPU kernels. In: OOPSLA, pp. 113–132. ACM (2012)
Blom, S., Darabi, S., Huisman, M.: Verification of loop parallelisations. In: Egyed, A., Schaefer, I. (eds.) FASE 2015. LNCS, vol. 9033, pp. 202–217. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46675-9_14
Blom, S., Huisman, M.: The VerCors Tool for verification of concurrent programs. In: Jones, C., Pihlajasaari, P., Sun, J. (eds.) FM 2014. LNCS, vol. 8442, pp. 127–131. Springer, Cham (2014). doi:10.1007/978-3-319-06410-9_9
Blom, S., Huisman, M., Mihelčić, M.: Specification and Verification of GPGPU programs. Sci. Comput. Program. 95, 376–388 (2014)
Blom, S., Huisman, M., Zaharieva-Stojanovski, M.: History-based verification of functional behaviour of concurrent programs. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 84–98. Springer, Cham (2015). doi:10.1007/978-3-319-22969-0_6
Bornat, R., Calcagno, C., O’Hearn, P.W., Parkinson, M.J.: Permission accounting in separation logic. In: POPL, pp. 259–270 (2005)
Cohen, E., Dahlweid, M., Hillebrand, M., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: a practical system for verifying concurrent C. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 23–42. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03359-9_2
Darabi, S., Blom, S.C.C., Huisman, M.: A verification technique for deterministic parallel programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 247–264. Springer, Cham (2017). doi:10.1007/978-3-319-57288-8_17
Huisman, M., Klebanov, V., Monahan, R., Tautschnig, M.: VerifyThis 2015: a program verification competition. Int. J. Softw. Tools Technol. Transfer (2016)
Jacobs, B., Smans, J., Philippaerts, P., Vogels, F., Penninckx, W., Piessens, F.: VeriFast: a powerful, sound, predictable, fast verifier for C and Java. In: Bobaru, M., Havelund, K., Holzmann, G.J., Joshi, R. (eds.) NFM 2011. LNCS, vol. 6617, pp. 41–55. Springer, Heidelberg (2011). doi:10.1007/978-3-642-20398-5_4
Leino, K.R.M., Müller, P., Smans, J.: Verification of concurrent programs with chalice. In: Aldini, A., Barthe, G., Gorrieri, R. (eds.) FOSAD 2007-2009. LNCS, vol. 5705, pp. 195–222. Springer, Heidelberg (2009). doi:10.1007/978-3-642-03829-7_7
Müller, P., Schwerhoff, M., Summers, A.J.: Viper: a verification infrastructure for permission-based reasoning. In: Jobstmann, B., Leino, K.R.M. (eds.) VMCAI 2016. LNCS, vol. 9583, pp. 41–62. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49122-5_2
O’Hearn, P.W.: Resources, concurrency and local reasoning. Theoret. Comput. Sci. 375(1–3), 271–307 (2007)
Oortwijn, W., Blom, S., Gurov, D., Huisman, M., Zaharieva-Stojanovski, M.: An abstraction technique for describing concurrent program behaviour. In: VSTTE (2017, to appear)
OpenMP Architecture Review Board, OpenMP API Specification for Parallel Programming. http://openmp.org/wp/. Accessed 18 Oct 2016
Vafeiadis, V.: Automatically proving linearizability. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 450–464. Springer, Heidelberg (2010). doi:10.1007/978-3-642-14295-6_40
Vafeiadis, V.: Concurrent separation logic and operational semantics. In: MFPS. ENTCS, vol. 276, pp. 335–351 (2011)
Acknowledgements
The work in this paper is partially supported by the ERC grant 258405 for the VerCors project, by the EU FP7 STREP 287767 project CARP, and by the NWO TOP 612.001.403 project VerDi.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 Springer International Publishing AG
About this paper
Cite this paper
Blom, S., Darabi, S., Huisman, M., Oortwijn, W. (2017). The VerCors Tool Set: Verification of Parallel and Concurrent Software. In: Polikarpova, N., Schneider, S. (eds) Integrated Formal Methods. IFM 2017. Lecture Notes in Computer Science(), vol 10510. Springer, Cham. https://doi.org/10.1007/978-3-319-66845-1_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-66845-1_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-66844-4
Online ISBN: 978-3-319-66845-1
eBook Packages: Computer ScienceComputer Science (R0)