key
key copied to clipboard
KeYProject
KeY Theorem Prover for Deductive Java Verification
## Description The SMT translation names a function parameter "length" to a function "length", which conflicts with the length function for objects. ## Reproducible always ### Steps to reproduce 1....
## Related Issue This pull request fixes #29. ## Intended Change A non-trivial (i.e, neither `true` nor `false`) diverges clause results in two contracts to be verified. Previously, there was...
## Related Issue This pull request addresses #3414. ## Intended Change Remove the old dialog to change taclet options. Taclet options can now be accessed through the new unified settings...
As discussed in a KaKeY meeting: We introduce a new "section" in KeY files dedicated to metadata: ``` \metadata ; ``` In contrast to `\settings` and `\proofObligation`, this section does...
This PR adds the newly introduced JML names for entities to KeY. Such labels are exploited inside the KeY's proof tree as branching labels. And may later become accessible in...
## Intended Change This PR fixes a slicing failure with a specific proof. In that particular case, the dynamically added taclet was slightly too different for the previous code to...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1723) where the discussions are preserved. ---- ## Description When trying to apply the `lesser-or-equal than distinction` rule to a floating point comparison on the...
## Description KeY used to have support for a model method modifier `no_state` indicating that a method must not at all read from the heap. Now, using `no_state` makes KeY...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1652) where the discussions are preserved. ---- There tend to be a lot of random runtime exceptions which should not ever occur. Instead of having...
This PR expands the proof caching infrastructure by introducing an external database of proofs. Proofs are currently added manually by the user to the database. The user may inspect the...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification