Abstract
We present a case-study of developing a simple software module using contracts, and rigorously verifying it for safety and functional correctness using two very different programming languages, that share the fact that both are extensively used in safety-critical development: SPARK and C/ACSL. This case-study, together with other investigations not detailed here, allows us to establish a comparison in terms of specification effort and degree of automation obtained with each toolset.
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
Preview
Unable to display preview. Download preview PDF.
References
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley Longman Publishing Co., Inc., Boston (2003)
Barnett, M., DeLine, R., Fähndrich, M., Jacobs, B., Leino, K.R.M., Schulte, W., Venter, H.: The Spec# Programming System: Challenges and Directions. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 144–152. Springer, Heidelberg (2008)
Baudin, P., Filliâtre, J.-C., Marché, C., Monate, B., Moy, Y., Prevosto, V.: ACSL: ANSI/ISO C Specification Language. CEA and INRIA. Preliminary design, version 1.4 (October 29, 2008)
Cohen, E., Dahlweid, M., Hillebrand, M.A., Leinenbach, D., Moskal, M., Santen, T., Schulte, W., Tobies, S.: VCC: A practical system for verifying concurrent C. In: Urban, C. (ed.) TPHOLs 2009. LNCS, vol. 5674, pp. 1–22. Springer, Heidelberg (2009)
Conchon, S., Contejean, E., Kanig, J.: Ergo: a Theorem Prover for Polymorphic First-order Logic Modulo Theories, LRI, Univ. Paris-Sud/CNRS, and INRIA (2006)
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a Theorem Prover for Program Checking. J. ACM 52(3), 365–473 (2005)
Filliâtre, J.-C., Marché, C.: The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)
Hoare, C.A.R.: An Axiomatic Basis For Computer Programming. Communications of the ACM 12, 576–580 (1969)
Jackson, P.B., Ellis, B.J., Sharp, K.: Using SMT Solvers to Verify High-integrity Programs. In: AFM 2007: Proceedings of the second workshop on Automated formal methods, pp. 60–68. ACM Press, New York (2007)
Leavens, G.T.: Tutorial on JML, the Java Modeling Language. In: Stirewalt, R.E.K., Egyed, A., Fischer, B. (eds.) Proceedings of ASE 2007, p. 573. ACM, New York (2007)
Marché, C.: Jessie: an Intermediate Language for Java and C Verification. In: Stump, A., Xi, H. (eds.) Proceedings of PLPV 2007. ACM, New York (2007)
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, Version 8.2 (2008)
Meyer, B.: Applying “Design by Contract”. IEEE Computer 25(10) (1992)
Reynolds, J.C.: Reasoning about arrays. Commun. ACM 22(5), 290–299 (1979)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brito, E., Sousa Pinto, J. (2010). Program Verification in SPARK and ACSL: A Comparative Case Study. In: Real, J., Vardanega, T. (eds) Reliable Software Technologiey – Ada-Europe 2010. Ada-Europe 2010. Lecture Notes in Computer Science, vol 6106. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-13550-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-13550-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-13549-1
Online ISBN: 978-3-642-13550-7
eBook Packages: Computer ScienceComputer Science (R0)