KeY-2.6.0 (2016-12-22)

Full Changelog: KeY-2.4.0...KeY-2.6.0

KeY-2.4.1 (2015-02-18)

Nothing known.

KeY-2.4.0 (2015-02-17)

• Information flow reasoning
• Full support for symbolic execution with bitwise operations
• Improved test case generation
• Improved user interface
• Support for CVC4 SMT solver backend

KeY-2.2.3 (2014-10-06)

• Fix concurrency issue introduced in 2.2.2

KeY-2.2.2 (2014-07-11)

• Support for CVC3 version 2.4.1 SMT backend
• Bug fixes

KeY-2.2.1 (2014-05-27)

• Test case generation using bounded SMT (requires Z3, OpenJML)
• Bug fixes

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

KeY-2.0.2 (2013-09-19)

• Support for latest versions of Z3 and CVC3
• Windows 8 compatibility
• Fix a soundness issue with types and heap access
• Various bug fixes

KeY-2.0.1 (2013-06-19)

• Bug fixes
  • Incompleteness with Java integer arithmetics
  • Command line mode fixes
  • various other

KeY-2.0.0 (2013-04-18)

• New explicit heap modeling
  • Data types for location sets and heaps
  • The heap is now a special (local) variable
  • Dynamic frames
  • JML extension for dynamic frame specification
  • Re-implementation of JavaCard transactions
• Verification of (primitive) recursive methods
• Sequence ADT
• Nearly complete JML support
  • model fields and methods
  • initially clauses and class axioms
  • measured_by clauses
  • accessible clauses
  • sum and product comprehension
  • the \bigint type, mixed integer semantics
  • weak purity by default
  • reachability predicate
  • \index and \values keywords for enhanced for-loops
• Escape to dynamic logic from within JML
• MonKeY batch mode
• GUI changes
  • new dialog to enter invariants interactively
  • search in sequents and proof trees
  • logical symbols in Unicode
• Runnable from command line without windowing system
• Improved integration of SMT solvers
  • SMT-LIB 2.0 backend interface
  • possible to run multiple solvers in parallel
  • support for integer division (Z3 only)

• 150 bug fixes

• Discontinued features
  • RTSJ support
  • Test case generation
  • OCL
  • Proof reuse