Abstract
A formal software verification system relies upon a software engineer writing mathematically precise specifications of intended behavior. Humans often introduce defects into such specifications. Techniques and tools capable of warning about common defects can help them develop correct specifications by finding subtle issues that would permit unintended behavior. New specification-checking techniques and a tool that implements them, SpecChec, are described.
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
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Tagore, A., Weide, B.W.: Automatically detecting inconsistencies in program specifications. In: Brat, G., Rungta, N., Venet, A. (eds.) NFM 2013. LNCS, vol. 7871, pp. 261–275. Springer, Heidelberg (2013)
Sitaraman, M., Adcock, B., Avigad, J., Bronish, D., Bucci, P., Frazier, D., Friedman, H., Harton, H., Heym, W., Kirschenbaum, J., Krone, J., Smith, H., Weide, B.: Building a push-button RESOLVE verifier: Progress and challenges. Formal Aspects of Computing 23(5), 607–626 (2011)
de Moura, L., Bjørner, N.S.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Adcock, B.M.: Working Towards the Verified Software Process. PhD thesis, The Ohio State University, Columbus, OH, USA (2010)
Westland, J.: The cost of errors in software development: evidence from industry. Journal of Systems and Software 62(1), 1–9 (2002)
Sitaraman, M., Weide, B.: Component-based software using RESOLVE. SIGSOFT Softw. Eng. Notes 19, 21–63 (1994)
Leino, K.R.M.: Dafny: An automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 348–370. Springer, Heidelberg (2010)
Leavens, G.T., Leino, K.R.M., Poll, E., Ruby, C., Jacobs, B.: JML: Notations and tools supporting detailed design in Java. In: OOPSLA 2000 Companion, pp. 105–106. ACM (2000)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: An overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Hoffman, D.: A Framework for Integrating Automated Software Verification Tools. Tech-Report (2012), ftp://ftp.cse.ohio-state.edu/pub/tech-report/2012/TR05.pdf
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
Hoffman, D., Tagore, A., Zaccai, D., Weide, B.W. (2014). Providing Early Warnings of Specification Problems. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_7
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)