Abstract
This paper presents a proof system for reasoning about execution time bounds for a core imperative programming language. Proof systems are defined for three different scenarios: approximations of the worst-case execution time, exact time reasoning, and less pessimistic execution time estimation using amortized analysis. We define a Hoare logic for the three cases and prove its soundness with respect to an annotated cost-aware operational semantics. Finally, we define a verification conditions (VC) generator that generates the goals needed to prove program correctness, cost, and termination. Those goals are then sent to the Easycrypt toolset for validation. The practicality of the proof system is demonstrated with an implementation in OCaml of the different modules needed to apply it to example programs. Our case studies are motivated by real-time and cryptographic software.
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
Similar content being viewed by others
References
Albert, E., et al.: Termination and cost analysis with COSTA and its user interfaces. Electron. Notes Theor. Comput. Sci. 258(1), 109–121 (2009). https://doi.org/10.1016/j.entcs.2009.12.008
Almeida, J.B., Frade, M.J., Pinto, J.S., de Sousa, S.M.: Rigorous Software Development - An Introduction to Program Verification. Undergraduate Topics in Computer Science. Springer, London (2011). https://doi.org/10.1007/978-0-85729-018-2
Apt, K.R., Olderog, E.: Fifty years of Hoare’s logic. Formal Aspects Comput. 31(6), 751–807 (2019). https://doi.org/10.1007/s00165-019-00501-3
Atkey, R.: Amortised resource analysis with separation logic. Log. Methods Comput. Sci. 7(2) (2011). https://doi.org/10.2168/LMCS-7(2:17)2011
Avanzini, M., Lago, U.D.: Automating sized-type inference for complexity analysis. Proc. ACM Program. Lang. 1(ICFP), 43:1–43:29 (2017). https://doi.org/10.1145/3110287
Barbosa, M., Barthe, G., Grégoire, B., Koutsos, A., Strub, P.Y.: Mechanized proofs of adversarial complexity and application to universal composability. In: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, CCS 2021, pp. 2541–2563. Association for Computing Machinery, New York (2021). https://doi.org/10.1145/3460120.3484548
Brockschmidt, M., Emmes, F., Falke, S., Fuhs, C., Giesl, J.: Alternating runtime and size complexity analysis of integer programs. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 140–155. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54862-8_10
Carbonneaux, Q., Hoffmann, J., Ramananandro, T., Shao, Z.: End-to-end verification of stack-space bounds for C programs. In: O’Boyle, M.F.P., Pingali, K. (eds.) ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, Edinburgh, United Kingdom, 09–11 June 2014, pp. 270–281. ACM (2014). https://doi.org/10.1145/2594291.2594301
Carbonneaux, Q., Hoffmann, J., Shao, Z.: Compositional certified resource bounds. In: Grove, D., Blackburn, S.M. (eds.) Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, Portland, OR, USA, 15–17 June 2015, pp. 467–478. ACM (2015). https://doi.org/10.1145/2737924.2737955
Dijkstra, E.W.: Guarded commands, non-determinacy and a calculus for the derivation of programs. In: Shooman, M.L., Yeh, R.T. (eds.) Proceedings of the International Conference on Reliable Software 1975, Los Angeles, California, USA, 21–23 April 1975, p. 2. ACM (1975). https://doi.org/10.1145/800027.808417
Gulwani, S., Mehra, K.K., Chilimbi, T.: SPEED: precise and efficient static estimation of program computational complexity. In: Proceedings of the 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, pp. 127–139. Association for Computing Machinery, New York (2009). https://doi.org/10.1145/1480881.1480898
Haslbeck, M.P.L., Nipkow, T.: Hoare logics for time bounds - a study in meta theory. In: Beyer, D., Huisman, M. (eds.) TACAS 2018, Part I. LNCS, vol. 10805, pp. 155–171. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-89960-2_9
Hoffmann, J., Das, A., Weng, S.: Towards automatic resource bound analysis for OCaml. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, 18–20 January 2017, pp. 359–373. ACM (2017). https://doi.org/10.1145/3009837.3009842
Hoffmann, J., Hofmann, M.: Amortized resource analysis with polynomial potential. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 287–306. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-11957-6_16
Hofmann, M., Jost, S.: Type-based amortised heap-space analysis. In: Sestoft, P. (ed.) ESOP 2006. LNCS, vol. 3924, pp. 22–37. Springer, Heidelberg (2006). https://doi.org/10.1007/11693024_3
Kaminski, B.L., Katoen, J., Matheja, C., Olmedo, F.: Weakest precondition reasoning for expected runtimes of randomized algorithms. J. ACM 65(5), 30:1–30:68 (2018). https://doi.org/10.1145/3208102
Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009). https://doi.org/10.1145/1538788.1538814
Loeckx, J., Sieber, K.: The Foundations of Program Verification, 2nd ed. Wiley-Teubner (1987)
Nielson, H.R.: A Hoare-like proof system for analysing the computation time of programs. Sci. Comput. Program. 9(2), 107–136 (1987). https://doi.org/10.1016/0167-6423(87)90029-3
Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer, London (2007). https://doi.org/10.1007/978-1-84628-692-6
Radiček, I., Barthe, G., Gaboardi, M., Garg, D., Zuleger, F.: Monadic refinements for relational cost analysis. Proc. ACM Program. Lang. 2(POPL) (2017). https://doi.org/10.1145/3158124
Serrano, A., López-García, P., Hermenegildo, M.V.: Resource usage analysis of logic programs via abstract interpretation using sized types. Theory Pract. Log. Program. 14, 739–754 (2014). https://doi.org/10.1017/S147106841400057X
Silva, A.C., Barbosa, M., Florido, M.: Execution time program verification with tight bounds (2022). Available from Arxiv
Simões, H.R., Vasconcelos, P.B., Florido, M., Jost, S., Hammond, K.: Automatic amortised analysis of dynamic memory allocation for lazy functional programs. In: Thiemann, P., Findler, R.B. (eds.) ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, Copenhagen, Denmark, 9–15 September 2012, pp. 165–176. ACM (2012). https://doi.org/10.1145/2364527.2364575
Tarjan, R.E.: Amortized computational complexity. SIAM J. Algebraic Discrete Methods 6(2), 306–318 (1985). https://doi.org/10.1137/0606031
Vasconcelos, P., Jost, S., Florido, M., Hammond, K.: Type-based allocation analysis for co-recursion in lazy functional languages. In: Vitek, J. (ed.) ESOP 2015. LNCS, vol. 9032, pp. 787–811. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-46669-8_32
Acknowledgment
This work was partially financially supported by Base Funding UIDB/00027/2020 of the Artificial Intelligence and Computer Science Laboratory – LIACC - funded by national funds through the FCT/MCTES (PIDDAC) and by INESC TEC.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG
About this paper
Cite this paper
Silva, A.C., Barbosa, M., Florido, M. (2023). Execution Time Program Verification with Tight Bounds. In: Hanus, M., Inclezan, D. (eds) Practical Aspects of Declarative Languages. PADL 2023. Lecture Notes in Computer Science, vol 13880. Springer, Cham. https://doi.org/10.1007/978-3-031-24841-2_4
Download citation
DOI: https://doi.org/10.1007/978-3-031-24841-2_4
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-031-24840-5
Online ISBN: 978-3-031-24841-2
eBook Packages: Computer ScienceComputer Science (R0)