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).
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
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.
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.
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.
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.
M. Cerioli, J. Meseguer. May I borrow your logic? Theoretical Computer Science, 173(2):311–347, 1997.
D. Hutter et al.: Verification Support Environment (VSE), Journal of High Integrity Systems, Vol. 1, 1996.
W. M. Farmer. An infrastructure for intertheory reasoning, In: D. McAllester, ed., Automated Deduction-CADE-17, LNCS, 1831:115–131, 2000.
Maya-webpage: http://www.dfki.de/~inka/maya.html.
J. McDonald, J. Anton. SPECWARE-Producing Software Correct by Construction. Kestrel Institute Technical Report KES.U.01.3., March 2001.
J. Meseguer. General logics, In Logic Colloquium 87, pages 275–329, North Holland, 1989.
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.
L. Paulson. Isabelle-A Generic Theorem Prover. LNCS 828. Springer, 1994.
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.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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