KeY-2.2.0 (2014-04-29)

• Counter example generation using bounded SMT (requires Z3)
• Increased JML support / JML extensions
  • block contracts (extension) / assert statements
  • \min and \max numerical quantifiers
  • changed default semantics of signals_only to include unchecked exceptions
  • model methods (new implementation)
  • old clause (variable binder in contract)
  • nearly everything parseable
• Verification of a large class of recursive methods
  • generalized variants to all ordered sets
• Proof obligations for specification well-definedness
• Term labels
• Rule triggers (extended taclet syntax)
• More efficient handling of heap disjointness and heap selects
• Improved reasoning about bounded sums/products
• User Interfaces
  • rule focus for inner nodes
  • improved search
  • detailed proof statistics
  • auto save and quick save features
  • keyboard shortcuts
• Reduced memory footprint
• A lot of bug fixes
• Java 8 compatibility
• Re-implemented .key parser