Logic and Formal Methods
Logic and Formal Methods
Logic and Formal Methods
Welcome to the Logic and Formal Methods Group
Staff

Verification of Memory Performance Contracts with KeY

  • Author(s):

    Christian Engel
  • Source:

    Technical Report, University of Karlsruhe, 2007

  • Determining the worst case memory consumption is an important issue for real-time Java applications. This work describes a methodology for formally verifying worst case memory performance constraints and proposes extensions to the Java Modeling Language (JML) facilitating better verifiability of JML performance specifications.