JuliaReach 是用于动态系统可达性计算的 Julia 生态系统。基于集合的可达性应用领域包括形式验证、控制器合成和在不确定模型参数或输入下的估计。如需更多背景信息，请在 JuliaReach zulip 流上联系我们。您也可以参考评论文章 用于可达性分析的集合传播技术。
难度: 中等。
描述。 LazySets 是 JuliaReach 的核心库。它提供了一种用几何集合进行符号计算的方法，重点关注延迟集合表示和高效的高维处理。该库已在文章 LazySets.jl: 可扩展的符号-数值集合计算 中进行了描述。
该项目的主要兴趣是实现利用集合结构的算法。典型的例子包括多面体和带状体（凸）、多项式带状体和泰勒模型（非凸），仅举几例。
预期结果。 目标是实现文献中某些高效的最新算法。该代码将进行文档化、测试和在基准测试中评估。具体任务可能包括（由候选人的兴趣驱动）：带状体 的高效顶点枚举；多项式带状体上的运算；带状体束 上的运算；不同集合类型之间的高效不相交性检查；复杂带状体。
预期时长。 175 小时。
推荐技能。 熟悉 Julia 和 Git/GitHub 是必须的。熟悉 LazySets 是推荐的。基本几何术语知识是值得赞赏的，但不是必需的。
导师: Marcelo Forets，Christian Schilling。
难度: 中等。
描述。 稀疏多项式带状体是一种新的非凸集合表示，非常适合于非线性动态系统的可达性分析。该项目是 GSoC'2022 - 使用稀疏多项式带状体的可达性 的延续，该项目在 LazySets 中实现了基础知识。
预期结果。 预计将在 ReachabilityAnalysis 中添加对动态系统可达性算法的有效 Julia 实现，该算法利用了多项式带状体。一个成功的项目应该
复制文章 [使用多项式带状体的具有不确定参数的线性系统的可达性分析
](https://dl.acm.org/doi/abs/10.1145/3575870.3587130) 中的结果。
该代码将在基准测试中进行文档化、测试和广泛评估。
对于有抱负的候选人，可以将它与 ClosedLoopReachability.jl 中实现的神经网络控制系统联系起来。
预期时长。 175 小时。
推荐技能。 熟悉 Julia 和 Git/GitHub 是必须的。熟悉提到的 Julia 包是值得赞赏的，但不是必需的。该项目不需要理论贡献，但需要阅读研究文献，因此建议具有一定的学术经验。
文献和相关包。 这段视频 解释了多项式带状体的概念（幻灯片 在这里）。相关理论在 这篇研究文章 中进行了描述。在 CORA 中存在一个 Matlab 实现（多项式带状体的实现可以在 这个文件夹 中找到）。
导师: Marcelo Forets，Christian Schilling。
难度: 中等。
描述。 ReachabilityAnalysis 是用于动态系统集合传播的 Julia 库。主要目标之一是处理具有混合离散-连续行为的系统（在文献中称为混合系统）。该项目将重点关注增强库的功能以及对用户生态系统的整体改进。
预期结果。 具体任务可能包括：针对混合系统的特定问题启发式方法；针对时变输入集的 API；流管下近似。该代码将在基准测试中进行文档化、测试和评估。如果感兴趣，也可以考虑与 ModelingToolkit.jl 集成。
预期时长。 175 小时。
推荐技能。 熟悉 Julia 和 Git/GitHub 是必须的。熟悉 LazySets 和 ReachabilityAnalysis 是值得欢迎的，但不是必需的。