key
key copied to clipboard
KeYProject
KeY Theorem Prover for Deductive Java Verification
- Adds missing taclets for intermediate JavaDL functions `unsignedshiftrightJlong`, `xorJlong`, `orJlong`, and `andJlong`. Without these, one cannot use the Java operators `>>>`, `^`, `|`, and `&` with parameters of type...
Tracking issue for *all* font scaling bugs. ## Description Changing the global font factor produces some weird artifacts. - [ ] Icon size does not adapt - [ ] Settings...
## Description As far as I can tell, it is not possible to express `int::seqGet` in a specification. `(int) \dl_seqGet` (or `(int)s[i]`) results in a moduloInt:  I have implemented...
I am currently going through bestpractises.dev for [KeY](https://www.bestpractices.dev/en/projects/7794). This is a site with best practises for open source projects. Our current status: [](https://www.bestpractices.dev/projects/7794) I want to use this...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/255) where the discussions are preserved. ---- * Mantis: [MT-1560](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1560) * Submitted on: 2015-08-04 by (at)mulbrich * Updated: 2015-09-25 * Assigned to: (at)mkirsten ### Description...
## Description When searching in a large sequent, a StackOverflowError is printed to stderr. ``` Exception in thread "AWT-EventQueue-0" java.lang.StackOverflowError at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088) at java.base/java.util.regex.Pattern$BmpCharPropertyGreedy.match(Pattern.java:4329) at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088) at java.base/java.util.regex.Pattern$BmpCharPropertyGreedy.match(Pattern.java:4329) at java.base/java.util.regex.Pattern$Slice.match(Pattern.java:4088)...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1212) where the discussions are preserved. ---- * Mantis: [MT-1129](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1129) * Submitted on: 2011-11-07 by (at)grahl * Updated: 2011-11-17 ### Description > Java allows you...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1459) where the discussions are preserved. ---- ## Description More complex JML storerefs like `array[*].field` cannot be parsed by KeY though they are (allegedly) valid...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/676) where the discussions are preserved. ---- * Mantis: [MT-1256](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1256) * Submitted on: 2012-12-19 by (at)mulbrich * Updated: 2012-12-19 ### Description > > A program...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/301) where the discussions are preserved. ---- * Mantis: [MT-1558](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1558) * Submitted on: 2015-08-01 by (at)rbubel * Updated: 2015-08-01 ### Description > Loading large proof...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification