Abstract
Though formal verification has been the holy grail of software validation, practical applications of verification run into two major challenges. The first challenge is in writing detailed specifications, and the second challenge is in scaling verification algorithms to large software. In this short paper, we present possible approaches for these problems. We propose using statistical techniques to raise the level of abstraction, and automate the tedium in writing detailed specifications. We propose combining testing with verification to help scalability.
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
Ball, T., Rajamani, S.K.: Automatically validating temporal safety properties of interfaces. In: Dwyer, M.B. (ed.) SPIN 2001. LNCS, vol. 2057, pp. 103–122. Springer, Heidelberg (2001)
Beckman, N.E., Nori, A.V., Rajamani, S.K., Simmons, R.J.: Proofs from tests. In: ISSTA 2008: International Symposium on Software Testing and Analysis, pp. 3–14. ACM Press, New York (2008)
Godefroid, P., Klarlund, N., Sen, K.: DART: Directed automated random testing. In: PLDI 2005: Programming Language Design and Implementation, pp. 213–223. ACM Press, New York (2005)
Godefroid, P., Nori, A.V., Rajamani, S.K., Tetali, S.: Compositional May-Must Program Analysis: Unleashing The Power of Alternation. Microsoft Research Technical Report MSR-TR-2009-2, Microsoft Research (2009)
Gulavani, B.S., Henzinger, T.A., Kannan, Y., Nori, A.V., Rajamani, S.K.: SYNERGY: A new algorithm for property checking. In: FSE 2006: Foundations of Software Engineering, pp. 117–127. ACM Press, New York (2006)
Livshits, B., Nori, A.V., Rajamani, S.K., Banerjee, A.: Merlin: Specification Inference for Explicit Information Flow Problems. In: PLDI 2009: Programming Language Design and Implementation. ACM Press, New York (to appear, 2009)
Nori, A.V., Rajamani, S.K., Tetali, S., Thakur, A.V.: The Yogi Project: Software Property Checking via Static Analysis and Testing. In: TACAS 2009: Tools and Algorithms for Constuction and Analysis of Systems. LNCS, vol. 5509, pp. 178–181. Springer, Heidelberg (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Nori, A., Rajamani, S.K. (2009). Verification, Testing and Statistics. In: Dubois, C. (eds) Tests and Proofs. TAP 2009. Lecture Notes in Computer Science, vol 5668. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02949-3_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-02949-3_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02948-6
Online ISBN: 978-3-642-02949-3
eBook Packages: Computer ScienceComputer Science (R0)