Skip to content

Issues: KeYProject/key

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Clear current search query, filters, and sorts
315 Open 2,803 Closed
315 Open 2,803 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

Block contracts are not applicable inside switch-statements Calculus 🐞 Bug P:NORMAL
#131 opened Dec 23, 2022 by wadoon
Obsolote / broken examples JML Parser 🐞 Bug P:NORMAL Proof Loading/Saving
#54 opened Dec 23, 2022 by wadoon
Programatic change of proof search strategy options 🐞 Bug P:LOW
#67 opened Dec 23, 2022 by wadoon
rules added during proof not in OSS domain 🐞 Bug P:NORMAL Prover Core
#69 opened Dec 23, 2022 by wadoon
Better feedback when using the proof search strategy Feature New feature or request GUI P:NORMAL
#76 opened Dec 23, 2022 by wadoon
Completeness gap with Dependency Contracts Calculus 🐞 Bug P:NORMAL
#81 opened Dec 23, 2022 by wadoon
exception during strategy execution Calculus 🐞 Bug P:NORMAL
#87 opened Dec 23, 2022 by wadoon
Decouple macros from the mediator to allow their use on side proofs Feature New feature or request P:NORMAL Prover Core
#108 opened Dec 23, 2022 by wadoon
JUnit tests have no timeout set 🛠 Maintenance Code quality and related things w/o functional changes P:LOW Test cases
#110 opened Dec 23, 2022 by wadoon
syntax of JML extensions should be reviewed Feature New feature or request JML (Semantics) P:LOW
#115 opened Dec 23, 2022 by wadoon
Strategy option for interactive contract selection Feature New feature or request P:NORMAL Prover Core
#121 opened Dec 23, 2022 by wadoon
more helpful message for unsupported JML syntax JML Parser P:LOW
#127 opened Dec 23, 2022 by wadoon
Non-trivial diverges clauses make you prove things twice. Feature New feature or request HacKeYthon Candidate Issue for HacKeYthon '25 JML (Semantics) P:LOW Small Student Task
#29 opened Dec 23, 2022 by wadoon
1
@unp1 @Drodt
Strategy option for automatically applying "strictlyPureMethodToUpdate" Feature New feature or request GUI P:NORMAL
#128 opened Dec 23, 2022 by wadoon
No Proof Obligations are available if Class and Source Path overlap KeY Parser 🐞 Bug P:LOW
#164 opened Dec 23, 2022 by wadoon
while loading a proof, the stop-button has no effect GUI P:LOW
#166 opened Dec 23, 2022 by wadoon
KeY modifier recognition defective JML Parser 🐞 Bug P:NORMAL
#167 opened Dec 23, 2022 by wadoon
Refactor variable substitution philosophy 🐞 Bug P:LOW
#168 opened Dec 23, 2022 by wadoon
'show known types' dialog with type hierarchy Feature New feature or request GUI P:LOW
#200 opened Dec 23, 2022 by wadoon
DL method contracts no longer maintained 🐞 Bug P:LOW
#204 opened Dec 23, 2022 by wadoon
Support parsing Java 7 source Feature New feature or request KeY Parser P:NORMAL
#216 opened Dec 23, 2022 by wadoon
Adapt KeY's user interface to use a StrategySettingsDefinition to create shown controls in tab "Proof Search Strategy" Feature New feature or request GUI P:HIGH
#217 opened Dec 23, 2022 by wadoon
Nested specification cases not correctly handled JML (Semantics) 🐞 Bug P:NORMAL
#220 opened Dec 23, 2022 by wadoon
Name clash for dependency-contracts for \inv in case of inheritance KeY Parser 🐞 Bug P:NORMAL
#223 opened Dec 23, 2022 by wadoon
static instance ghost fields are possible, but should not be JML Parser 🐞 Bug
#3585 opened Mar 13, 2025 by mattulbrich
ProTip! What’s not been updated in a month: updated:<2025-02-16.