Abstract
Program analysis and verification techniques have made great strides, yet, as every researcher in the field will admit it is easy to find a program and property for which a given technique is not cost-effective. Investigating the conventional wisdom that programs are mostly correct, we have observed that even failed program analyses usually produce a wealth of information about the parts of the program that operate correctly. Leveraging this information can help focus subsequent analysis and verification activities to make them more cost-effective.
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 subscriptionsReferences
Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM 50, 63–69 (2003)
Randell, B., Lee, P.A., Treleaven, P.C.: Reliability issues in computing system design. ACM Comput. Surv. 10, 123–165 (1978)
DeMillo, R.A., Lipton, R.J., Sayward, F.G.: Hints on test data selection: Help for the practicing programmer. Computer 11, 34–41 (1978)
Dwyer, M.B., Purandare, R.: Residual dynamic typestate analysis: exploiting static analysis results to reformulate and reduce the cost of dynamic analysis. In: 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 2007), Atlanta, Georgia, USA, November 5-9, 2007, pp. 124–133 (2007)
Strom, R.E., Yemini, S.: Typestate: A programming language concept for enhancing software reliability. IEEE Trans. Softw. Eng. 12, 157–171 (1986)
Lal, A., Kidd, N., Reps, T.W., Touili, T.: Abstract error projection. In: Riis Nielson, H., Filé, G. (eds.) SAS 2007. LNCS, vol. 4634, pp. 200–217. Springer, Heidelberg (2007)
Wolfe, M.: High performance compilers for parallel computing. Addison-Wesley, Reading (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dwyer, M.B., Purandare, R. (2008). Residual Checking of Safety Properties. In: Havelund, K., Majumdar, R., Palsberg, J. (eds) Model Checking Software. SPIN 2008. Lecture Notes in Computer Science, vol 5156. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-85114-1_1
Download citation
DOI: https://doi.org/10.1007/978-3-540-85114-1_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-85113-4
Online ISBN: 978-3-540-85114-1
eBook Packages: Computer ScienceComputer Science (R0)