Skip to main content
SpringerLink
Log in

Maintenance of Formal Software Developments by Stratified Verification

  • Conference paper
  • First Online:
Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2002)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 2514))

Abstract

The development of industrial-size software is an evolutionary process based on structured specifications. In a formal setting, specification and verification are intertwined. Specifications are amended either to add new functionality or to fix bugs detected during the verification process. In this paper we propose a system to maintain the verification of formal developments. It exploits the structure of the specification to reveal and eliminate redundant proof obligations and therefore constitutes itself a verification system in-the-large. Proofs in this system are represented as explicit proof objects allowing the system to adjust or reuse them in case the specification is changed.

This work was supported by the German Ministry for Education and Technology (BMBF).

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

Access this chapter

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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. S. Autexier, D. Hutter, H. Mantel, A. Schairer. System description: InKa 5.0-a logic voyager. In H. Ganzinger (Ed.): 16th International Conference on Automated Deduction, Springer, LNAI 1632, 1999.

    Google Scholar 

  2. S. Autexier, D. Hutter, H. Mantel, and A. Schairer. Towards an evolutionary formal software-development using CASL. In C. Choppy and D. Bert, editors, Proceedings Workshop on Algebraic Development Techniques, WADT-99. Springer, LNCS 1827, 2000.

    Google Scholar 

  3. S. Autexier, T. Mossakowski. Integrating HOL-Casl into the Development Graph Manager Maya. In A. Armando (Ed.) Frontiers of Combining Systems (Fro-CoS’02), Santa Margherita Ligure, Italy, Springer LNAI, April, 2002.

    Google Scholar 

  4. CoFI Language Design Task Group. The common algebraic specification language (Casl)-summary, 1998. Version 1.0 and additional Note S-9 on Semantics, available from http://www.brics.dk/Projects/CoFI.

  5. M. Cerioli, J. Meseguer. May I borrow your logic? Theoretical Computer Science, 173(2):311–347, 1997.

    Article  MATH  MathSciNet  Google Scholar 

  6. D. Hutter et al.: Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 1996.

    Google Scholar 

  7. W. M. Farmer. An infrastructure for intertheory reasoning, In: D. McAllester, ed., Automated Deduction-CADE-17, LNCS, 1831:115–131, 2000.

    Chapter  Google Scholar 

  8. Maya-webpage: http://www.dfki.de/~inka/maya.html.

  9. J. McDonald, J. Anton. SPECWARE-Producing Software Correct by Construction. Kestrel Institute Technical Report KES.U.01.3., March 2001.

    Google Scholar 

  10. J. Meseguer. General logics, In Logic Colloquium 87, pages 275–329, North Holland, 1989.

    Google Scholar 

  11. T. Mossakowski, S. Autexier, and D. Hutter: Extending Development Graphs With Hiding. In H. Hußmann (Ed.), Proceedings of Fundamental Approaches to Software Engineering (FASE 2001), Italy. LNCS 2029, 269–283. Springer, 2001.

    Chapter  Google Scholar 

  12. L. Paulson. Isabelle-A Generic Theorem Prover. LNCS 828. Springer, 1994.

    MATH  Google Scholar 

  13. W. Reif: The KIV-approach to Software Verification, In KORSO: Methods, Languages, and Tools for the Construction of Correct Software-Final Report, LNCS 1009, 339–368. Springer, 1995.

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. German Research Center for Artificial Intelligence, Stuhlsatzenhausweg 3, D-66123, Saarbruecken, Germany

    Serge Autexier & Dieter Hutter

Authors
  1. Serge Autexier
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dieter Hutter
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Abteilung für Theoretische Informatik, Institut für Algebra und Diskrete Mathematik, Wiedner Hauptstr. 8-10, 1040, Wien, Austria

    Matthias Baaz

  2. Department of Computer Science, University of Manchester, Kilburn Building, Oxford Road, Manchester, M13, 9PL, UK

    Andrei Voronkov

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Autexier, S., Hutter, D. (2002). Maintenance of Formal Software Developments by Stratified Verification. In: Baaz, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2002. Lecture Notes in Computer Science(), vol 2514. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36078-6_3

Download citation

  • DOI: https://doi.org/10.1007/3-540-36078-6_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00010-5

  • Online ISBN: 978-3-540-36078-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation