key
key copied to clipboard
KeYProject
KeY Theorem Prover for Deductive Java Verification
## Description I was testing other basic cases and came across this problem, I didn't seem to find any issue that had already been reported. `@ assignable \nothing;` should allow...
## Description It used to be that the formula which becomes the target of a drag-and-drop activity was highlighted in green. This is no longer the case since commit 4759370f719ed506746e7a2a13832eac48cfc6c1...
## Description The keyboard shortcut for the auto mode (ctrl + space) cannot be used when the proof tree or the task tree is focused. ### Steps to reproduce 1....
This PR adds a new option to the proof tree to "linearize symbolic execution". This option changes the proof tree to be slightly more linear. In effect, the "Normal Execution"...
## Related Issue This PR fixes a bug that prevented the interactive provision of a loop invariant. ## Intended Change It should be possible to enter loop invariants manually. ##...
## Please describe your proposal in a ONE sentence > One sentence describing your idea In order to work more smoothly, it would be good to be able to edit...
## Description When I use "assignable" in the Key Editor, I have my proof which fails, yet the method does not modify anything. If assignable is removed, it works. This...
## Description In the current version of KeY, the integer semantics with explicit overflow checks as introduced by #3027 are broken on at least 3 levels: 1) The annotation `/*@...
## Please describe your proposal in a ONE sentence Allow rulesets (heuristics) to be defined with a list of additional arguments ## Underlying problem For several rulesets the strategies have...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1532) where the discussions are preserved. ---- ## Reproducible Always ### Steps to reproduce 1. Load some proof obligation. An interaction log named, e.g., "bumpy...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification