Skip to content
KeY Documentation
LLM support
Initializing search
key-docs
Home
User Guide
Developer Guide
Historical
KeY Enhancement Proposals
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. Supported Language Features
8. Supported Language Features
Java Coverage
9. 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
Thread Safety and Determinism
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
Add a Term Label
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
Proof search
Proof search
The Rule Application Pipeline
Taclet Matching
Strategy Costs and the Cost-Band Ladder
Multi-Core Proving
Terms and parsing
Terms and parsing
The KeY Parser
Term Labels
Proofs and external solvers
Proofs and external solvers
Proof Loading and Saving
SMT Translation
Counterexample Generation
Legacy
Legacy
Extending Recoder (obsolete)
7. Testing
7. Testing
Proved Rules
RunAllProofs
Deterministic Test Order (outdated)
Parser Message Tests
CI Infrastructure
8. Writing Documentation
9. Appendices
9. Appendices
Strategy Cost Tables
Historical
Historical
Eclipse plugins (unsupported)
Eclipse plugins (unsupported)
KeY basics
SED
Stubby
KeY IDE
MonKeY
Starter
VisualDBC
JML Editing
Resources
KeY Enhancement Proposals
KeY Enhancement Proposals
KEP-1: Taclet-Generating Transformers
Table of contents
Features
Configuration
How to use
LLM support
⚠ not yet verified
Features
¶
Configuration
¶
How to use
¶
Back to top