Abstract
Symbolic execution is a useful technique in formal verification and testing. In this paper, we propose to use it to estimate the performance of programs. We first extract a set of paths (either randomly or systematically) from the program, and then obtain a weighted average of the performance of the paths. The weight of a path is the number of input data that drive the program to execute along the path, or the size of the input space that corresponds to the path. As compared with traditional benchmarking, the proposed approach has the benefit that it uses more points in the input space. Thus it is more representative in some sense. We illustrate the new approach with a sorting algorithm and a selection algorithm.
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
Boyer, R., Moore, S.: A fast string matching algorithm. Comm. ACM 20, 762–772 (1977)
Cole, R.: Tight bounds on the complexity of the Boyer-Moore string matching algorithm. In: Proc. of the 2nd Symp. on Discrete Algorithms (SODA 1991), pp. 224–233 (1991)
Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proc. of the Int’l Symposium on Software Testing and Analysis (ISSTA 2012), pp. 166–176 (2012)
Hoare, C.A.R.: Proof of a program: FIND. Commun. ACM 14(1), 39–45 (1971)
King, J.C.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)
Knuth, D.E.: The Stanford GraphBase: A Platform for Combinatorial Computing. ACM Press (1994), http://www-cs-faculty.stanford.edu/~knuth/sgb.html
Liu, S., Zhang, J.: Program analysis: from qualitative analysis to quantitative analysis. In: Proc. of the 33rd Int’l Conf. on Software Engineering (ICSE 2011), pp. 956–959 (2011)
Ma, F., Liu, S., Zhang, J.: Volume computation for Boolean combination of linear arithmetic constraints. In: Schmidt, R.A. (ed.) CADE-22. LNCS, vol. 5663, pp. 453–468. Springer, Heidelberg (2009)
Zhang, J.: Quantitative analysis of symbolic execution. Presented at the 28th Int’l Computer Software and Applications Conf. (COMPSAC 2004) (2004)
Zhang, J.: Constraint solving and symbolic execution. In: Meyer, B., Woodcock, J. (eds.) VSTTE 2005. LNCS, vol. 4171, pp. 539–544. Springer, Heidelberg (2008)
Zhang, J., Liu, S., Ma, F.: A tool for computing the volume of the solution space of SMT(LAC) constraints, draft (January 2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Zhang, J. (2013). Performance Estimation Using Symbolic Data. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Theories of Programming and Formal Methods. Lecture Notes in Computer Science, vol 8051. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39698-4_21
Download citation
DOI: https://doi.org/10.1007/978-3-642-39698-4_21
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39697-7
Online ISBN: 978-3-642-39698-4
eBook Packages: Computer ScienceComputer Science (R0)