KeYProject/key: Nightly Release

Read full text
Authors: unp1, danielgrahl, Alexander Weigl, Mattias Ulbrich, mi.ki, Arne Keller, jwiesler, Wolfram Pfeifer, lichtemo, BookWood, Daniel Drodt, David Giessing
+17 more Florian Lanzinger, alicia, simongreiner, Tobias Reinhold, rheimbach, zhao-nan, pschmitt27, Christopher Beckmann, Mattias Ulbrich, PumpkinPieTroelf, T. Lippert, Lukas Grätz, Wojciech Mostowski, vladrich, SeeVella, Carsten Csiky, Jonas Krämer
Cited by: 0

Abstract

What's Changed Breaking Changes 🗲 Removal of Triple, and Quadruple by @wadoon in https://github.com/KeYProject/key/pull/3529 Use KeYParser.g4 for parsing proof scripts by @wadoon in https://github.com/KeYProject/key/pull/3021 Migration to java.nio.Path by @wadoon in https://github.com/KeYProject/key/pull/3618 Exciting New Features 🎉 Renovation of the TestCase generation by @wadoon in https://github.com/KeYProject/key/pull/3388 Features Proposing a more flexible lexing framework by @mattulbrich in https://github.com/KeYProject/key/pull/3537 highlight current line in issue editor pane by @mattulbrich in https://github.com/KeYProject/key/pull/3573 Improved treatment of final fields by @mattulbrich in https://github.com/KeYProject/key/pull/3495 Enable SMT focus goals (unsat cores) for CVC5 by @FliegendeWurst in https://github.com/KeYProject/key/pull/3594 SMT test cases rework by @WolframPfeifer in https://github.com/KeYProject/key/pull/3592 Isabelle Translation by @BookWood7th in https://github.com/KeYProject/key/pull/3514 Introducing some structure for model method bodies by @mattulbrich in https://github.com/KeYProject/key/pull/3571 Linearized symbolic execution in proof tree by @FliegendeWurst in https://github.com/KeYProject/key/pull/3237 Bug Fixes Add conversion rules for Float/Double negation by @WolframPfeifer in https://github.com/KeYProject/key/pull/3520 Fix #3524 by @Drodt in https://github.com/KeYProject/key/pull/3525 Fixing the broken automode by @mattulbrich in https://github.com/KeYProject/key/pull/3533 Fix #3452 by @wadoon in https://github.com/KeYProject/key/pull/3540 Adding a rule for exactInstance of final types. (fixes #3389) by @mattulbrich in https://github.com/KeYProject/key/pull/3543 fixing lexing to support static invariants by @mattulbrich in https://github.com/KeYProject/key/pull/3583 Fixed obtaining results from CVC4 and cvc5 by @WolframPfeifer in https://github.com/KeYProject/key/pull/3593 Fix Java version in nightlydeploy.yml by @wadoon in https://github.com/KeYProject/key/pull/3598 Fix exception in javac extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3609 fix testMakeFilenameRelativeWindows by @wadoon in https://github.com/KeYProject/key/pull/3619 Disable relative path test on Windows by @wadoon in https://github.com/KeYProject/key/pull/3629 Fix SMT ApplyAction not pruning when undoing by @BookWood7th in https://github.com/KeYProject/key/pull/3606 Fix NPE using KeY command line interface caused by Java NIO by @wadoon in https://github.com/KeYProject/key/pull/3643 FIX: URGENT: Changes in Gradle 9 results into non-execution of custom test tasks. by @wadoon in https://github.com/KeYProject/key/pull/3653 fix css for sequentview syntaxhighlightning by @wadoon in https://github.com/KeYProject/key/pull/3645 Allow true in more JML expressions by @mattulbrich in https://github.com/KeYProject/key/pull/3664 Fix NPE in dependency contract feature (caused by pulled out expression) by @unp1 in https://github.com/KeYProject/key/pull/3675 Fix Information Flow Proof Loading for KeY Jar File by @Drodt in https://github.com/KeYProject/key/pull/3678 Enable assertion for :key.ui:run by @wadoon in https://github.com/KeYProject/key/pull/3682 Fix proof task tree forced white background. by @wadoon in https://github.com/KeYProject/key/pull/3663 Dependencies Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3516 Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3517 Bump the gradle-deps group with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3527 Bump JetBrains/qodana-action from 2024.2.3 to 2024.2.6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3526 Bump the github-actions-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3531 Bump the gradle-deps group across 1 directory with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3536 Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3577 Bump the gradle-deps group across 1 directory with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3581 Bump the gradle-deps group across 1 directory with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3589 Bump the gradle-deps group across 1 directory with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3596 Bump the gradle-deps group with 3 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3603 Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3617 Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3627 Bump the gradle-deps group with 7 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3646 Bump the gradle-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3649 Bump the gradle-deps group with 5 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3655 Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3656 Bump gradle/actions from 4 to 5 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3667 Bump the gradle-deps group with 8 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3666 Bump the gradle-deps group with 9 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3679 Bump actions/upload-artifact from 4 to 5 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3680 Bump actions/checkout from 5 to 6 in the github-actions-deps group by @dependabot[bot] in https://github.com/KeYProject/key/pull/3694 Bump the gradle-deps group across 1 directory with 6 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3695 Bump the gradle-deps group with 4 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3704 Bump the github-actions-deps group with 2 updates by @dependabot[bot] in https://github.com/KeYProject/key/pull/3705 Other Changes Set the Java Release Version to 21 by @wadoon in https://github.com/KeYProject/key/pull/3522 Using semantic version (SemVer) scheme for KeY by @wadoon in https://github.com/KeYProject/key/pull/3523 fixes Location#compareTo(Location) by @BookWood7th in https://github.com/KeYProject/key/pull/3519 RuleApp interface for all external solvers (prep for #3514) by @BookWood7th in https://github.com/KeYProject/key/pull/3521 Missing project description for two sub-modules by @wadoon in https://github.com/KeYProject/key/pull/3528 Re-enable sonarqube for quality assessment by @wadoon in https://github.com/KeYProject/key/pull/3488 Also depend on checker-qual artifact by @wmdietl in https://github.com/KeYProject/key/pull/3535 Added BoyerMoore.key by @TudorBalan in https://github.com/KeYProject/key/pull/3558 repair the axiom generation for adts defined in JavaDL by @mattulbrich in https://github.com/KeYProject/key/pull/3556 Fix/Improve KeY example application by @samysweb in https://github.com/KeYProject/key/pull/3562 Cleanup: Removal of key.api package by @wadoon in https://github.com/KeYProject/key/pull/3550 fix #3553 by @MarcoScaletta in https://github.com/KeYProject/key/pull/3560 Fix #3563 by @Drodt in https://github.com/KeYProject/key/pull/3566 Fix line number alignment in SMT interface by @BookWood7th in https://github.com/KeYProject/key/pull/3559 Add documentation for soundDefaultContracts feature by @flo2702 in https://github.com/KeYProject/key/pull/3574 Use a custom Github action for setting up the SMT solvers by @wadoon in https://github.com/KeYProject/key/pull/3569 Improve JavaDocs for Qualifier, SyntaxElement by @Drodt in https://github.com/KeYProject/key/pull/3579 Warn on missing SMT solvers if flag is set by @wadoon in https://github.com/KeYProject/key/pull/3600 Extract Taclets and Prover Main Loop to ncore by @Drodt in https://github.com/KeYProject/key/pull/3578 Fix for a performance regression by @unp1 in https://github.com/KeYProject/key/pull/3607 Fix Checker Framework Errors by @Drodt in https://github.com/KeYProject/key/pull/3610 Fix deprecated Gradle build syntax, update shadow dependency by @Drodt in https://github.com/KeYProject/key/pull/3612 Fix graphviz configuration of slicing extension by @FliegendeWurst in https://github.com/KeYProject/key/pull/3613 Remove duplicate NewDependingOn class by @Drodt in https://github.com/KeYProject/key/pull/3615 Generalize Taclet Implementation by @Drodt in https://github.com/KeYProject/key/pull/3605 Rename core Term/Operator/... to JTerm/JOperator... to avoid name clashes with ncore Term/Operator/... by @Drodt in https://github.com/KeYProject/key/pull/3616 Move Taclet matching infrastructure to ncore by @unp1 in https://github.com/KeYProject/key/pull/3608 Using FlatLAF for a modern look and feel by @wadoon in https://github.com/KeYProject/key/pull/3599 Cleanup: Remove antlr3 + antlr2 from the classpath by @wadoon in https://github.com/KeYProject/key/pull/3624 Fix some indirect dependencies by updating used plugins that introduce them by @unp1 in https://github.com/KeYProject/key/pull/3626 Test if matrix over modules are a good thing by @wadoon in https://github.com/KeYProject/key/pull/3622 Cleanup: Use Standard Tech for Test Fixtures by @wadoon in https://github.com/KeYProject/key/pull/3551 Remove unnecessary (and harmful) license plugin by @Drodt in https://github.com/KeYProject/key/pull/3628 Reduce raw usage of classes by @Drodt in htt

Publication details

Journal / source
Zenodo (CERN European Organization for Nuclear Research)
Publication date
5 January 2026