Abstract
CloudMake is a software utility that automatically builds executable programs and libraries from source code—a modern Make utility. Its design gives rise to a number of possible optimizations, like cached builds, and the executables to be built are described using a functional programming language. This paper formally and mechanically verifies the correctness of central CloudMake algorithms.
The paper defines the CloudMake language using an operational semantics, but with a twist: the central operation exec is defined axiomatically, making it pluggable so that it can be replaced by calls to compilers, linkers, and other tools. The formalization and proofs of the central CloudMake algorithms are done entirely in Dafny, the proof engine of which is an SMT-based program verifier.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development—Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer (2004)
Boyer, R.S., Hunt Jr., W.A.: Function memoization and unique object representation for ACL2 functions. In: ACL2 Theorem Prover and its Applications, pp. 81–89. ACM (2006)
Feldman, S.I.: Make—A program for maintaining computer programs. Software—Practice and Experience 9(4), 255–265 (1979)
Heydon, A., Levin, R., Mann, T., Yu, Y.: Software Configuration Management Using Vesta. Monographs in Computer Science. Springer (2006)
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)
Leino, K.R.M.: Automating induction with an SMT solver. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 315–331. Springer, Heidelberg (2012)
Leino, K.R.M.: Automating theorem proving with SMT. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 2–16. Springer, Heidelberg (2013)
Leino, K.R.M., Wüstholz, V.: The Dafny integrated development environment. In: Workshop on Formal-IDE (to appear, 2014)
Lerner, S., Millstein, T., Chambers, C.: Automatically proving the correctness of compiler optimizations. In: PLDI, pp. 220–231. ACM (2003)
Leroy, X.: Formal verification of a realistic compiler. Communications of the ACM 52(7), 107–115 (2009)
McCarthy, J., Painter, J.: Correctness of a compiler for arithmetic expressions. In: Proceedings of Applied Mathematica. Mathematical Aspects of Computer Science, vol. 19, pp. 33–41. American Mathematical Society (1967)
Milner, R., Weyhrauch, R.: Proving compiler correctness in a mechanized logic. Machine Intelligence 7, 51–72 (1972)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Christakis, M., Leino, K.R.M., Schulte, W. (2014). Formalizing and Verifying a Modern Build Language. In: Jones, C., Pihlajasaari, P., Sun, J. (eds) FM 2014: Formal Methods. FM 2014. Lecture Notes in Computer Science, vol 8442. Springer, Cham. https://doi.org/10.1007/978-3-319-06410-9_43
Download citation
DOI: https://doi.org/10.1007/978-3-319-06410-9_43
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06409-3
Online ISBN: 978-3-319-06410-9
eBook Packages: Computer ScienceComputer Science (R0)