KeYHeap

"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).

Publications

• 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

Presentation Slides

• 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)

Download the Latest KeY Development Version

[Internal wiki page]

Highlights

• 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)

Some features of KeY 1.6 currently unsupported in KeYHeap

• 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

Contact

Benjamin Weiß