"KeYHeap" is the working title of a major revision of the KeY system that is currently under development. At its core, KeYHeap is a deductive verifier for sequential Java programs wrt. specifications written in a crossover between JML and dynamic frames. Unlike all KeY versions <= 1.6, KeYHeap uses a heap model like that of typical Boogie-based verifiers (in particular VeriCool and Dafny, which also use dynamic frames style specifications).

*Most important: Deductive Verification of Object-Oriented Software: Dynamic Frames, Dynamic Logic and Predicate Abstraction*- PhD thesis, Karlsruhe Institute of Technology, February 2011- Dynamic Frames in Java Dynamic Logic - post-conference proceedings of FoVeOOS 2010, LNCS 6528, Springer, January 2011
- Dynamic Frames in Java Dynamic Logic: Formalisation and Proofs - technical report 2010-11, Department of Computer Science, KIT, June 2010

- Dynamic Frames in Java Dynamic Logic - talk at FoVeOOS 2010, Paris (June 29, 2010)
- Dynamic Frames in JML - talk at 9th KeY Symposium 2010, Gernsbach (May 25, 2010)
- Dynamic Frames in KeY - talk at research seminar formal methods, Karlsruhe (January 29, 2010)
- Explicit Representation of the Heap - talk at 8th KeY Symposium 2009, Speyer (May 19, 2009)

Java web start: | Run KeY now |

Bytecode: | Current-bin.tgz |

Sourcecode: | Current-src.tgz |

- New heap model
- Sorts "Heap" and "Field", functions "select", "store", "create", "anon", program variable "heap"
- "o.f" means "select(heap, o, f)" instead of "f(o)"
- Functions with heap as argument instead of
*location dependent functions* - Set-typed terms instead of
*location descriptors* - More straightforward encoding of the correctness of modifies clauses, using quantification over locations

- Reasoning about location sets (empty sets, singleton sets, union, intersection, set difference, set comprehension)
- Simplified model of object allocation
- Allocation "new MyClass()" takes an unspecified object satisfying "o.<created>=FALSE & MyClass::exactInstance(o)=TRUE"
- No need for allocation counters "MyClass.<nextToCreate>" and object enumerators "MyClass::<get>"
- Constant domain assumption still in effect

- Adapted JML frontend and proof management
- Type \locset in specifications (dynamic frames)
- Model fields and dependencies
- Modifies clauses implictly allow object allocation and initialisation
- Invariants as model field \inv instead of
*visible state semantics*or*observed state semantics* - Method contract rule discharges whole method call including dynamic dispatch (behavioural subtyping)
- Type \seq in specifications (finite mathematical sequences)

- Rule-based update simplification
- Ca. 20 rewrite taclets (using two special, but simple "variable conditions") instead of one large built-in rule
- Optional "one-step simplification": Meta-rule that eagerly applies rewrite rules in the "concrete" and "simplify" categories as a single proof step
- One-step simplification plays similar role as update simplifier in normal KeY, but is not limited to updates

- Simplified representation of integers
- One sort "int" instead of the hierarchy of "int", "jbyte", "jchar", "jint", "jlong", "jshort", "integerDomain"
- Different choices for handling overflows (ignore, check, be Java-faithful) still supported
- ArrayStoreException still handled correctly

- Code refactoring
- Cleaned up implementation of core data structures (sorts, operators, terms, formulas, updates)

- Meta variables, meta variable constraints
- JavaCard transactions, "throughout" modalities
- RTSJ
- Test case generation
- Specification extraction
- Correctness proof obligations for taclets
- Proof visualisation, visual debugger
- UML/OCL front end
- Proof reuse
- ODL
- Eclipse plugin

Benjamin Weiß