key
key copied to clipboard
KeYProject
KeY Theorem Prover for Deductive Java Verification
The purpose of this PR is to repair the overflow checking of KeY and thus fix #3352. TODO: * [x] fix creation of branches for overflow checking * [x] fix...
## Please describe your proposal in a ONE sentence > One sentence describing your idea Selection of a JML line in the source view leads to highlighting all formulas of...
## Description > Please describe your concern in detail! In JML you can't use userdefined \sorts from .key files ``` \javaSource "."; \sorts{ Tupel; } \chooseContract ``` ```java class A{...
* [ ] KeY diverged from the second KeY book, Macro is not there anymore.  * [ ] Incorrect tooltip: Macro was removed?!  @unp1 @mattulbrich
Alternative version for #3324 using the settings instead of storing it in the proof. Using a path encoding of the current node (list of child indexes) and a run-length encoding...
This PR is an alternative to #3272, it only includes the optimizations. See the commits in this branch for details. Short description of each optimization: - replaceKnown is called only...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/680) where the discussions are preserved. ---- * Mantis: [MT-1294](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1294) * Submitted on: 2013-04-30 by (at)greiner * Updated: 2013-05-14 ### Description > After creating a...
Abbreviations are built-in to the KeY system, but this construct is not very popular. This may be to their volatility: you are not able to store, and reuse them on...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/992) where the discussions are preserved. ---- * Mantis: [MT-1402](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1402) * Submitted on: 2014-01-21 by (at)wasser * Updated: 2014-02-14 ### Description > A loop invariant...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1494) where the discussions are preserved. ---- # Overview Verifying programs that use iterators in KeY is currently very difficult. There are neither taclets for...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification