Discussions

• 2 You must be logged in to vote

  🙏

  How to prove created-ness of variable that is reassigned in loop?

  Calculus

  FliegendeWurst asked Jan 27, 2026 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  How to prove static invariant (of an enum) in different heap?

  Calculus

  FliegendeWurst asked Dec 11, 2025 in Q&A · Answered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Issue Importing .proof Files in KeY: "Could Not Resolve BigInteger.ONE"

  JDavidCE2022 asked Feb 10, 2025 in Q&A · Unanswered

  

  

  3
• 2 You must be logged in to vote

  📣

  KeY is on Github.

  Infrastructure Changes to the Github configurations, repository or other non-source stuff

  wadoon announced Jan 30, 2023 in Announcements

  

  

  1
• 1 You must be logged in to vote

  🙏

  Help for using the existence of an array that fulfills a condition.

  fab918 asked Dec 16, 2023 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  is it allowed to assign a JML expression containing a quantifier to a ghost variable?

  JavaJMLParser

  waynee95 asked Sep 5, 2023 in Q&A · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  What is variant for in the invariant configurator?

  JML (Semantics)

  waynee95 asked Sep 5, 2023 in Q&A · Answered

  

  

  2
• 1 You must be logged in to vote

  💬

  License header in each file

  Infrastructure Changes to the Github configurations, repository or other non-source stuff

  wadoon started Jul 21, 2023 in General

  

  

  2
• 1 You must be logged in to vote

  💡

  New JML specification elements

  JML (Semantics)

  wadoon started Feb 6, 2023 in Ideas

  

  

  1