key
key copied to clipboard
KeYProject
KeY Theorem Prover for Deductive Java Verification
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/806) where the discussions are preserved. ---- * Mantis: [MT-1111](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1111) * Submitted on: 2011-08-29 by (at)mulbrich * Updated: 2013-01-18 * Assigned to: (at)mulbrich ### Description...
## Related Issue This pull request answers to issue #1723. ## Intended Change Floats and doubles are currently incorrectly insufficiently handled when they appear in one expression. Casts need to...
## Description When you try to start a proof of a dependency contract of a model field that contains `\strictly_nothing`, an exception is thrown during generation of the proof obligation....
This issue tries to track changes for KeY that arise of the current discussion for the next JML ref version on Github. * Add `\old`, `\pre`, and `\before`, and `\invariant_for(obj,...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/110) where the discussions are preserved. ---- * Mantis: [MT-1378](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1378) * Submitted on: 2013-10-28 by (at)grahl * Updated: 2013-10-28 ### Description > JUnit test cases...
## Description Sometimes the simplifyUpdate1/simplifyUpdate2 rules ignore updates, specifically to `LoctionVaribale`s. This seems to be caused by preceding pruning. In my case something like `{ ... || heapBefore_foo:=heap || ......
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1559) where the discussions are preserved. ---- ## Description It is possible to prove `false` using the `observerDependency` taclets. The problem is that this/these taclet/s...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1418) where the discussions are preserved. ---- * Mantis: [MT-1375](http://i12www.ira.uka.de/~klebanov/mantis/view.php?id=1375) * Submitted on: 2013-10-23 by (at)klebanov * Updated: 2015-01-16 ### Description > In the attached...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1536) where the discussions are preserved. ---- To understand the functionality of updates I have been playing around and found the following bug in parsing...
This issue was created at [git.key-project.org](https://git.key-project.org/key/key/-/issues/1538) where the discussions are preserved. ---- The loading of key files is not homogenous. A special type of files, the logic-datatype files (LDT) are...
Metadata
Owner
Metadata
KeY Theorem Prover for Deductive Java Verification