Abstract
This position paper is based on presentations given at the Grand Challenge workshops held at Gresham College in March 2004 and in Newcastle in July 2005. It reports some of our experience from building the SPARK language and its verification tools. We argue that the provision of an unambiguous semantics for a programming language is crucial if the verification framework is to be sound, deep and efficient. Secondly, we offer some reflections on the (mostly non-technical) barriers that we encounter in trying to deploy SPARK within organizations. Finally, we try to set some goals for future work.
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
Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison Wesley, Reading (2003)
Miné, A.: Relational abstract domains for the detection of floating-point run-time errors. In: Schmidt, D. (ed.) ESOP 2004. LNCS, vol. 2986, pp. 3–17. Springer, Heidelberg (2004)
Steel, G.: The importance of Non-theorems and Counterexamples in Program Verification. University of Edinburgh. Position paper for this workshop
Humphrey, W.: Winning with Software: An Executive Strategy. Addison-Wesley, Reading (2001)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
The SPARK Team (2008). Languages, Ambiguity, and Verification. In: Meyer, B., Woodcock, J. (eds) Verified Software: Theories, Tools, Experiments. VSTTE 2005. Lecture Notes in Computer Science, vol 4171. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69149-5_52
Download citation
DOI: https://doi.org/10.1007/978-3-540-69149-5_52
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-69147-1
Online ISBN: 978-3-540-69149-5
eBook Packages: Computer ScienceComputer Science (R0)