Skip to content
KeY Documentation
LLM support
Initializing search
key-docs
Home
User Guide
Developer Guide
Historical
KeY Documentation
key-docs
Home
User Guide
User Guide
1. Getting Started
1. Getting Started
Installation
Loading JML Contracts
Proving JML Contracts
Appendix: Tips and Background
2. Working with the Prover
2. Working with the Prover
The Taclet Match Dialog
Excluding Goals from Automation
Proof Exploration
Comparing Proof Nodes
Linearized Proof Tree
Proof Caching
Proof Slicing
3. Structuring Verification Projects
3. Structuring Verification Projects
The Classpath Directive
Programs with Generics
User-Defined Data Types
JavaDL Escapes in JML
4. Proof Scripts
4. Proof Scripts
Language Constructs
Command Reference
Script Variables
Macros
Linear Proof Scripts
Proof Scripts in JML
Historical Notes (2015)
5. SMT Solvers
5. SMT Solvers
Adding SMT Solvers
6. Bridges to Other Tools
6. Bridges to Other Tools
7. Language Reference
7. Language Reference
JML Grammar
The KeY Language
KeY's Java Extensions
8. FAQ
Release Notes
Developer Guide
Developer Guide
1. Architecture
2. Building KeY
3. Working on the Code
3. Working on the Code
Coding Conventions
Formatting with Spotless
Logging
4. Extending KeY
4. Extending KeY
Overview
How-Tos (verified recipes)
How-Tos (verified recipes)
Add an Extension Module
Add a Menu Entry
Add a Toolbar
Add Taclets
Add a Proof Macro
Add a Script Command
Writing Taclets
Polarity Triggers for Rewrite Taclets
GUI Extension Points
Script Commands in Depth
Adding SMT Solvers
Event Listeners
5. Using KeY as a Library
5. Using KeY as a Library
KeY in External Projects
6. Internals
6. Internals
The Rule Application Pipeline
Performance Optimizations (3.1)
Multi-Core Proving
Proof Loading and Saving
The KeY Parser
SMT Translation
Counterexample Generation
Extending Recoder (obsolete)
7. Testing
7. Testing
Proved Rules
RunAllProofs
Deterministic Test Order (outdated)
Parser Message Tests
CI Infrastructure
8. Writing Documentation
Historical
Historical
Eclipse plugins (unsupported)
Eclipse plugins (unsupported)
KeY basics
SED
Stubby
KeY IDE
MonKeY
Starter
VisualDBC
JML Editing
Resources
Table of contents
Features
Configuration
How to use
LLM support
⚠ not yet verified
Features
¶
Configuration
¶
How to use
¶
Back to top