KORSO: Methods, Languages, and Tools for the Construction of Correct Software

1. Front Matter

   PDF

2. Correct software: From experiments to applications

   • Manfred Broy, Martin Wirsing

   Pages 1-24

3. A method for the development of correct software

   • Peter Pepper, Martin Wirsing, Ralph Betschko, Manfred Broy, Sabine Dick, Klaus Didrich et al.

   Pages 25-57

4. Realizing sets by hash tables

   • Peter Pepper, Ralph Betschko, Sabine Dick, Klaus Didrich

   Pages 58-73

5. Event automata as a generic model of reactive systems

   • G. Michele Pinna, Axel Poigné

   Pages 74-91

6. On object-oriented design and verification

   • C. Lewerentz, Th. Lindner, A. Rüping, E. Sekerinski

   Pages 92-111

7. Design of modular software systems with reuse

   • Stefan Gastinger, Rolf Hennicker, Robert Stabl

   Pages 112-127

8. AVL trees revisited: A case study in Spectrum

   • R. Hettler, D. Nazareth, F. Regensburger, O. Slotosch

   Pages 128-147

9. KORSO reference languages concepts and application domains

   • H. -D. Ehrich

   Pages 148-172

10. How to cope with the Spectrum of Spectrum

    • U. Wolter, K. Didrich, F. Cornelius, M. Klar, R. Wessäly, H. Ehrig

    Pages 173-189

11. A fine-grain sort discipline and its application to formal program construction

    • Jochen Burghardt

    Pages 190-204

12. TROLL light — The language and its development environment

    • M. Gogolla, S. Conrad, G. Denker, R. Herzig, N. Vlachantonis, H. -D. Ehrich

    Pages 205-220

13. Formalization of algebraic specification in the development language Deva

    • Thomas Santen, Florian Kammüller, Stefan Jähnichen, Martin Beyer

    Pages 221-238

14. Construction and deduction methods for the formal development of software

    • F. W. von Henke, A. Dold, H. Rueß, D. Schwier, M. Strecker

    Pages 239-254

15. Experiences with a specification environment

    • Jacques Loeckx, Jörg Zeyer

    Pages 255-267

16. Towards correct, efficient and reusable transformational developments

    • Bernd Krieg-Brückner, Junbo Liu, Hui Shi, Burkhard Wolff

    Pages 268-284

17. The verification system Tatzelwurm

    • Peter Deussen, Alex Hansmann, Thomas Käufl, Stefan Klingenbeck

    Pages 285-298

18. Seduct — A proof compiler for first order logic

    • Karl Stroetmann

    Pages 299-316

19. Traverdi — Transformation and verification of distributed systems

    • J. Bohn, H. Hungar

    Pages 317-338

20. The Kiv-approach to software verification

    • Wolfgang Reif

    Pages 339-368

This book constitutes the final report of the work carried out in the project KORSO ("Korrekte Software") funded by the German Federal Ministry for Research and Technology. KORSO is an evolutionary, prototype-oriented project aimed at improving the theoretical foundations of quality-driven software engineering and at implementing known techniques for applications of practical relevance.
The 21 strictly refereed papers presented are organized in five sections on methods for correctness, languages, development systems and logical frameworks, tools, and case studies. In addition, the preface and introductory paper give valuable background information and a concise state-of-the-art overview.

• Compiler
• Correct Software
• Dependable Systems
• Formal Software Development
• Formal Verification
• Formale Verifikation
• Sicherheitsrelevante Systeme
• Softwarequalität
• automata
• design
• distributed systems
• formal method
• formal specification
• logic
• verification

Policies and ethics