Abstract
Executable formal contracts help verify a program at runtime when static verification fails. However, these contracts may be prohibitively slow to execute, especially when they describe the transformations of data structures. In fact, often an efficient data structure operation with O(log(n)) running time executes in O(n log(n)) when naturally written specifications are executed at run time.
We present a set of techniques that improve the efficiency of run-time checks by orders of magnitude, often recovering the original asymptotic behavior of operations. Our implementation first removes any statically verified parts of checks. Then, it applies a program transformation that changes recursively computed properties into data structure fields, ensuring that properties are evaluated no more than once on a given data structure node. We present evaluation of our techniques on the Leon system for verification of purely functional programs.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Blanc, R.W., Kneuss, E., Kuncak, V., Suter, P.: An overview of the Leon verification system: Verification by translation to recursive functions. In: Scala Workshop (2013)
Bodden, E., Lam, P., Hendren, L.: Partially evaluating finite-state runtime monitors ahead of time. ACM Trans. Program. Lang. Syst. 34(2), 7:1–7:52 (2012)
Flanagan, C.: Hybrid type checking. In: Morrisett, J.G., Jones, S.L.P. (eds.) POPL, pp. 245–256. ACM (2006)
Hughes, J.: Lazy memo-functions. In: Jouannaud, J.-P. (ed.) FPCA 1985. LNCS, vol. 201, pp. 129–146. Springer, Heidelberg (1985)
Michie, D.: Memo functions and machine learning. Nature 218(5136), 19–22 (1968)
Okasaki, C.: Functional data structures. In: Launchbury, J., Sheard, T., Meijer, E. (eds.) AFP 1996. LNCS, vol. 1129, pp. 131–158. Springer, Heidelberg (1996)
Shankar, A., Bodik, R.: Ditto: automatic incrementalization of data structure invariant checks (in Java). ACM SIGPLAN Notices 42, 310–319 (2007)
Suter, P., Köksal, A.S., Kuncak, V.: Satisfiability modulo recursive programs. In: Yahav, E. (ed.) SAS 2011. LNCS, vol. 6887, pp. 298–315. Springer, Heidelberg (2011)
Swift, T., Warren, D.S.: Xsb: Extending Prolog with tabled logic programming. Theory and Practice of Logic Programming 12(1-2), 157–187 (2012)
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
Koukoutos, E., Kuncak, V. (2014). Checking Data Structure Properties Orders of Magnitude Faster. In: Bonakdarpour, B., Smolka, S.A. (eds) Runtime Verification. RV 2014. Lecture Notes in Computer Science, vol 8734. Springer, Cham. https://doi.org/10.1007/978-3-319-11164-3_22
Download citation
DOI: https://doi.org/10.1007/978-3-319-11164-3_22
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-11163-6
Online ISBN: 978-3-319-11164-3
eBook Packages: Computer ScienceComputer Science (R0)