Cover Image
Read Now

Verification of Object-Oriented Software. The KeY Approach Foreword by K. Rustan M. Leino

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 who...

Full description

Bibliographic Details
Other Authors: Beckert, Bernhard (Editor), Hähnle, Reiner (Editor), Schmitt, Peter H. (Editor)
Format: eBook
Language:English
Published: Berlin, Heidelberg Springer Berlin Heidelberg 2007, 2007
Edition:1st ed. 2007
Series:Lecture Notes in Artificial Intelligence
Subjects:
Compilers (computer Programs)
Computer Science Logic And Foundations Of Programming
Compilers And Interpreters
Software Engineering
Computer Science
Artificial Intelligence
Formal Languages And Automata Theory
Machine Theory
Online Access:
Collection: Springer eBooks 2005- - Collection details see MPG.ReNa
Table of Contents:
  • A New Look at Formal Methods for Software Construction
  • A New Look at Formal Methods for Software Construction
  • I: Foundations
  • First-Order Logic
  • Dynamic Logic
  • Construction of Proofs
  • II: Expressing and Formalising Requirements
  • Formal Specification
  • Pattern-Driven Formal Specification
  • Natural Language Specifications
  • Proof Obligations
  • From Sequential Java to Java Card
  • III: Using the KeY System
  • Using KeY
  • Proving by Induction
  • Java Integers
  • Proof Reuse
  • IV: Case Studies
  • The Demoney Case Study
  • The Schorr-Waite-Algorithm
  • Appendices
  • Predefined Operators in Java Card DL
  • The KeY Syntax

Similar Items