Skip to main content
SpringerLink
Log in
Book cover

Verification of Object-Oriented Software. The KeY Approach

Foreword by K. Rustan M. Leino

  • Book
  • © 2007

Overview

Editors:
  1. Bernhard Beckert
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  2. Reiner Hähnle
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

  3. Peter H. Schmitt
    View editor publications

    You can also search for this editor in PubMed   Google Scholar

Part of the book series: Lecture Notes in Computer Science (LNCS, volume 4334)

Part of the book sub series: Lecture Notes in Artificial Intelligence (LNAI)

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

Access this book

Log in via an institution
eBook USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book USD 109.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

Other ways to access

Licence this eBook for your library

Institutional subscriptions

Table of contents (17 chapters)

  1. Front Matter

    Download chapter PDF

  2. A New Look at Formal Methods for Software Construction

    1. A New Look at Formal Methods for Software Construction

      • Reiner Hähnle
      Pages 1-18

  3. Part I: Foundations

    1. Front Matter

      Pages 19-19
      Download chapter PDF

    2. First-Order Logic

      • Martin Giese
      Pages 21-68

    3. Dynamic Logic

      • Bernhard Beckert, Vladimir Klebanov, Steffen Schlager
      Pages 69-177

    4. Construction of Proofs

      • Philipp Rümmer
      Pages 179-242

  4. Part II: Expressing and Formalising Requirements

    1. Front Matter

      Pages 243-243
      Download chapter PDF

    2. Formal Specification

      • Andreas Roth, Peter H. Schmitt
      Pages 245-294

    3. Pattern-Driven Formal Specification

      • Richard Bubel, Reiner Hähnle
      Pages 295-315

    4. Natural Language Specifications

      • Kristofer Johannisson
      Pages 317-333

    5. Proof Obligations

      • Andreas Roth
      Pages 335-374

    6. From Sequential Java to Java Card

      • Wojciech Mostowski
      Pages 375-405

  5. Part III: Using the KeY System

    1. Front Matter

      Pages 407-407
      Download chapter PDF

    2. Using KeY

      • Wolfgang Ahrendt
      Pages 409-451

    3. Proving by Induction

      • Angela Wallenburg
      Pages 453-479

    4. Java Integers

      • Steffen Schlager
      Pages 481-505

    5. Proof Reuse

      • Vladimir Klebanov
      Pages 507-529

  6. Part IV: Case Studies

    1. Front Matter

      Pages 531-531
      Download chapter PDF

    2. The Demoney Case Study

      • Wojciech Mostowski
      Pages 533-568

    3. The Schorr-Waite-Algorithm

      • Richard Bubel
      Pages 569-587
Back to top

Keywords

About this book

Long gone are the days when program veri?cation was a task carried out merely by hand with paper and pen. For one, we are increasingly interested in proving actual program artifacts, not just abstractions thereof or core algorithms. The programs we want to verify today are thus longer, including whole classes and modules. As we consider larger programs, the number of cases to be considered in a proof increases. The creative and insightful parts of a proof can easily be lost in scores of mundane cases. Another problem with paper-and-pen proofs is that the features of the programming languages we employ in these programs are plentiful, including object-oriented organizations of data, facilities for specifying di?erent c- trol ?ow for rare situations, constructs for iterating over the elements of a collection, and the grouping together of operations into atomic transactions. These language features were designed to facilitate simpler and more natural encodings of programs, and ideally they are accompanied by simpler proof rules. But the variety and increased number of these features make it harder to remember all that needs to be proved about their uses. As a third problem, we have come to expect a higher degree of rigor from our proofs. A proof carried out or replayed by a machine somehow gets more credibility than one that requires human intellect to understand.

Reviews

From the reviews:

"This book is a collection of work by different authors on software verification. The context of the book is the key project, which aims to build a verification of the systems based on model checking. The book features the widely used specification languages: object constraint language (OCL) and Java modeling language (JML). … this book is a good resource for graduate students and researchers … ." (S. Balaraman, Computing Reviews, December, 2007)

Bibliographic Information

Publish with us

Policies and ethics

Back to top

Search

Navigation