Skip to main content
SpringerLink
Log in
Book cover

International Conference on Interactive Theorem Proving

ITP 2014: Interactive Theorem Proving pp 17–26Cite as

Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK

  • Conference paper

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8558))

Abstract

This paper presents a retrospective of our experiences with applying theorem proving to the verification of SPARK programs, both in terms of projects and the technical evolution of the language and tools over the years.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnes, J., Chapman, R., Johnson, R., Widmaier, J., Cooper, D., Everett, B.: Engineering the Tokeneer enclave protection software. In: 1st IEEE International Symposium on Secure Software Engineering (March 2006)

    Google Scholar 

  2. Barnes, J.: SPARK: The Proven Approach to High Integrity Software. Altran Praxis (2012)

    Google Scholar 

  3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Berghofer, S.: Verification of dependable software using SPARK and isabelle. In: SSV, pp. 15–31 (2011)

    Google Scholar 

  5. Bobot, F., Filliâtre, J.C., Marché, C., Paskevich, A.: Why3: Shepherd your herd of provers. In: Boogie 2011: First International Workshop on Intermediate Verification Languages, Wrocław, Poland, pp. 53–64 (August 2011), http://proval.lri.fr/publications/boogie11final.pdf

  6. Brain, M., Schanda, F.: A lightweight technique for distributed and incremental program verification. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 114–129. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  7. Chapman, R., Botcazou, E., Wallenburg, A.: SPARKSkein: A formal and fast reference implementation of skein. In: Simao, A., Morgan, C. (eds.) SBMF 2011. LNCS, vol. 7021, pp. 16–27. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  8. Conchon, S., Contejean, E., Kanig, J.: Ergo: A theorem prover for polymorphic first-order logic modulo theories (2006), http://ergo.lri.fr/papers/ergo.ps

  9. Cullyer, W., Goodenough, S., Wichmann, B.: The choice of computer languages for use in safety-critical systems. Software Engineering Journal 6(2), 51–58 (1991)

    Article  Google Scholar 

  10. D’Silva, V., Haller, L., Kroening, D.: Abstract conflict driven learning. In: POPL, pp. 143–154 (2013)

    Google Scholar 

  11. Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. ACM Trans. Program. Lang. Syst. 9(3), 319–349 (1987), http://doi.acm.org/10.1145/24039.24041

    Article  MATH  Google Scholar 

  12. Fitzpatrick, B., et al.: Memcached - a distributed memory object caching system (2003), http://memcached.org

  13. German, A.: Software static code analysis lessons learned. Crosstalk 16(11) (2003)

    Google Scholar 

  14. Horwitz, S., Reps, T., Binkley, D.: Interprocedural slicing using dependence graphs. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation, PLDI 1988, pp. 35–46. ACM, New York (1988), http://doi.acm.org/10.1145/53990.53994

    Chapter  Google Scholar 

  15. Jackson, P.B., Passmore, G.O.: Proving SPARK verification conditions with smt solvers. Technical Report, University of Edinburgh (2009)

    Google Scholar 

  16. King, S., Hammond, J., Chapman, R., Pryor, A.: Is proof more cost-effective than testing? IEEE Transactions on Software Engineering 26(8), 675–686 (2000)

    Article  Google Scholar 

  17. Mehta, N.: Cve-2014-0160 (April 2014)

    Google Scholar 

  18. Middleton, P., Sutton, J.: Lean Software Strategies: Proven Techniques for Managers and Developers. Productivity Press (2005)

    Google Scholar 

  19. O’Neill, I.: Logic Programming Tools and Techniques for Imperative Program Verification. Ph.D. thesis, University of Southampton (1987)

    Google Scholar 

  20. Parnas, D.L., Madey, J., Iglewski, M.: Precise documentation of well-structured programs. IEEE Transactions on Software Engineering 20(12), 948–976 (1994)

    Article  Google Scholar 

  21. Rolfe, M.: How technology is transforming air traffic management, http://nats.aero/blog/2013/07/how-technology-is-transforming-air-traffic-management

  22. RTCA: DO-178C: Software considerations in airborne systems and equipment certification (2011)

    Google Scholar 

  23. RTCA: DO-333: Formal methods supplement to do-178c and do-278a (2011)

    Google Scholar 

  24. Schanda, F., Brain, M.: Using answer set programming in the development of verified software. In: ICLP (Technical Communications), pp. 72–85 (2012)

    Google Scholar 

  25. Schneier, B., Ferguson, N., Lucks, S., Whiting, D., Bellare, M., Kohno, T., Walker, J., Callas, J.: The skein hash function family. Submission to NIST (Round 3) (2010)

    Google Scholar 

  26. http://www.skein-hash.info

  27. http://muen.codelabs.ch

  28. Woodcock, J., Aydal, E.G., Chapman, R.: The Tokeneer Experiments. In: Reflections on the Work of CAR Hoare, pp. 405–430. Springer (2010)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Altran UK Limited, 22 St Lawrence Street, Bath, BA1 1AN, United Kingdom

    Roderick Chapman & Florian Schanda

Authors
  1. Roderick Chapman
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Florian Schanda
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. NICTA, Sydney, NSW, Australia

    Gerwin Klein

  2. University of Wyoming, Laramie, WY, USA

    Ruben Gamboa

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Chapman, R., Schanda, F. (2014). Are We There Yet? 20 Years of Industrial Theorem Proving with SPARK. In: Klein, G., Gamboa, R. (eds) Interactive Theorem Proving. ITP 2014. Lecture Notes in Computer Science, vol 8558. Springer, Cham. https://doi.org/10.1007/978-3-319-08970-6_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-08970-6_2

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-08969-0

  • Online ISBN: 978-3-319-08970-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation