Abstract
For critical software development, containers such as lists, vectors, sets or maps are an attractive alternative to ad-hoc data structures based on pointers. As standards like DO-178C put formal verification and testing on an equal footing, it is important to give users the ability to apply both to the verification of code using containers. In this paper, we present a definition of containers whose aim is to facilitate their use in certified software, using modern proof technology and novel specification languages. Correct usage of containers and user-provided correctness properties can be checked either by execution during testing or by formal proof with an automatic prover. We present a formal semantics for containers and an axiomatization of this semantics targeted at automatic provers. We have proved in Coq that the formal semantics is consistent and that the axiomatization thereof is correct.
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
The Coq Proof Assistant, http://coq.inria.fr
DO-178B: Software considerations in airborne systems and equipment certification (1982)
http://www.open-do.org/wp-content/uploads/2011/01/main.long.pdf
Blanc, N., Groce, A., Kroening, D.: Verifying C++ with STL containers via predicate abstraction. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2007, pp. 521–524. ACM, USA (2007)
Bouillaguet, C., Kuncak, V., Wies, T., Zee, K., Rinard, M.: Using First-Order Theorem Provers in the Jahob Data Structure Verification System. In: Cook, B., Podelski, A. (eds.) VMCAI 2007. LNCS, vol. 4349, pp. 74–88. Springer, Heidelberg (2007)
Conchon, S., Contejean, E.: The Alt-Ergo automatic theorem prover (2008), http://alt-ergo.lri.fr/
de Moura, L., Bjørner, N.: Z3, An Efficient SMT Solver, http://research.microsoft.com/projects/z3/ .
Detlefs, D., Nelson, G., Saxe, J.B.: Simplify: a theorem prover for program checking. J. ACM 52(3), 365–473 (2005)
Dillig, I., Dillig, T., Aiken, A.: Precise reasoning for programs using containers. In: Proceedings of the 11th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL (January 2011)
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)
Gregor, D., Schupp, S.: STLlint: lifting static checking from languages to libraries. Softw. Pract. Exper. 36, 225–254 (2006)
Kosiuczenko, P.: An abstract machine for the old value retrieval. In: Bolduc, C., Desharnais, J., Ktari, B. (eds.) MPC 2010. LNCS, vol. 6120, pp. 229–247. Springer, Heidelberg (2010)
Rushby, J.: Formalism in safety cases. In Chris Dale and Tom Anderson, editors, Making Systems Safer. In: Dale, C., Anderson, T. (eds.) Making Systems Safer: Proceedings of the Eighteenth Safety-Critical Systems Symposium, pp. 3–17. Springer, Heidelberg (2010)
Schwarz, J.T.: Programming with sets: an introduction to SETL. Lavoisier (October 1986)
Souyris, J., Wiels, V., Delmas, D., Delseny, H.: Formal Verification of Avionics Software Products. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 532–546. Springer, Heidelberg (2009)
Zee, K., Kuncak, V., Rinard, M.: Full functional verification of linked data structures. In: Proceedings of the 2008 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2008, pp. 349–361. ACM, New York (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dross, C., Filliâtre, JC., Moy, Y. (2011). Correct Code Containing Containers. In: Gogolla, M., Wolff, B. (eds) Tests and Proofs. TAP 2011. Lecture Notes in Computer Science, vol 6706. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-21768-5_9
Download citation
DOI: https://doi.org/10.1007/978-3-642-21768-5_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-21767-8
Online ISBN: 978-3-642-21768-5
eBook Packages: Computer ScienceComputer Science (R0)