This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Wolfgang Ahrendt
A grouping.
The specification side of the KeY work rather than the proving side: how a logic should talk about objects that do not exist yet, how a specification is written in JML, and how deductive verification and symbolic execution meet. All four records are in verifying-real-java, and all share the KeY book with the other people working on that tool.
4 references
Integrating deductive verification and symbolic execution for abstract object creation in dynamic logic
Stijn de Gouw and others (2016) · Software and Systems Modeling
Deductive Software Verification – The KeY Book
Mattias Ulbrich and others (2016) · Springer
Formal Specification with JML
Marieke Huisman and others (2014) · Karlsruhe Institute of Technology
Abstract Object Creation in Dynamic Logic: To Be or Not to Be Created
Wolfgang Ahrendt and others (2009) · FM 2009: Formal Methods · Springer