Bio-inspired Mechanism and Model Exploration of Software Aging
处于网络环境中的软件系统在长时间运行过程中会出现性能下降、可用性下降甚至崩溃的现象，即软件老化。人们对软件老化现象的研究已有15年多的历史，但大多数文献都是把软件作为一个黑箱来研究，没有一个文献揭示出我们所知的软件老化的基本机制。通过分析生物老化和软件老化之间的特点，我们发现了一些有趣的共同点，弥合了这两个看似无关的现象之间的差距。生物学中的自由基老化理论也适用于探讨软件老化的机制和模型。本文发现了软件老化中的“软件自由基”与生物老化中的自由基是等价的。在我们的研究中，“软件自由基”的积累是软件老化的根本原因。利用生物老化中的自由基建模方法，给出了一个基于反馈环的软件老化动力学模型。虽然本文没有对该建模方法给出足够的理论证明，但实践结果表明，该反馈环模型能够准确地描述软件老化的动力学过程。为了进一步验证老化机制，我们提出了几个软件复兴战略，侧重于清洁的“软件自由基”。结果表明，通过加强负反馈回路或弱化正反馈回路，可以有效地减缓软件老化。本文首次尝试通过跨学科研究来回答“软件如何老化”的问题。利用本文的结论，人们可以设计出更好的软件系统，或者在长时间运行中保持系统的高性能。
2014-08-27 cs.SE
Control software analysis, part II: Closed-loop analysis
对闭环控制软件属性的分析和适当的文档与对运行开环的同一软件的分析有许多不同的方面。出现了物理系统表示的问题，并且期望这样的表示保持独立于控制程序的表示。为此，提出了一个并发程序表示的工厂和控制过程，虽然闭环系统是足够的串行化，使顺序分析。在处理闭环系统特性的同时，还通过示例显示了非线性的特殊处理如何从控制规范分析扩展到代码分析。
2008-12-10 cs.PL cs.SE
QFL: Data-Driven Feedback Loop to Manage Quality in Agile Development
背景：质量需求（QR）描述了期望的系统质量，在软件项目的成功中起着重要的作用。在敏捷软件开发（ASD）的背景下，主要目标是快速交付功能，QR通常定义不清，并且在开发过程中没有很好地解决。软件分析工具通过度量与质量相关的软件方面来帮助控制质量，以支持QR管理过程中的决策者。目的：本研究的目标是探索集成一个具体的软件分析工具，Q-Rapids工具，以评估软件质量和支持QR管理过程的好处。方法：在技术转让项目的背景下，Softeam公司在其开发过程中集成了Q-Rapids工具。我们举办了一系列研讨会，邀请了Modelio产品开发部门的Softeam成员参加。结果如下：我们提出的质量反馈环（QFL）过程中集成在软件开发过程中，以控制完整的QR生命周期，从启发到验证。由于在Softeam中实施了QFL，Modelio的团队成员强调了将数据分析工具与项目规划工具集成的好处，以及项目经理可以控制整个过程以做出最终决策的事实。结论：从业者可以从软件分析工具的集成中受益，作为其软件开发工具链的一部分，以控制软件质量。QFL的实施提高了组织的质量，软件分析和项目规划工具的集成也改善了团队之间的沟通。
2021-02-11 cs.SE
Human-in-the-loop online just-in-time software defect prediction
针对现有在线即时软件缺陷预测忽略SQA人员交互的问题，提出人在回路方法并设计结合k折分布式自助法与Wilcoxon检验的评估框架，经10个GitHub项目验证可提升预测性能与评估可信度。
2023-08-25 cs.SE
Lost in Code Generation: Reimagining the Role of Software Models in AI-driven Software Engineering
TU Wien（维也纳工业大学）
该研究针对AI生成软件存在的缺陷，提出从AI生成系统中恢复软件模型，区分智能体与人类反思循环，将软件模型作为连接现有软件工程与AI驱动开发的桥梁，拓展了软件模型的作用。
2026-08-28 cs.SE
Embedded Software Development with Digital Twins: Specific Requirements for Small and Medium-Sized Enterprises
本文通过访谈中小型企业，发现实时性要求、安全顾虑及硬件访问限制阻碍了软件在环开发，但数字孪生仍被视为提升质量与定制化的潜力所在。
2023-09-17 cs.SE
A language for feedback loops in self-adaptive systems: Executable runtime megamodels
自适应软件的开发需要设计适当的反馈循环，其中自适应逻辑控制底层软件。适配逻辑通常通过使用表示底层软件的运行时模型以及诸如在这些运行时模型上操作的分析和规划的步骤来描述适配。为了系统地解决这种相互作用，已经提出了运行时大模型，其是将自身的运行时模型作为其元素并且还捕获多个运行时模型之间的关系的特定运行时模型。在本文中，我们更进一步，并提出了一个建模语言的运行时megamodels，大大简化了开发的自适应逻辑提供了一个特定领域的建模方法和运行时解释器的这部分自适应系统。这通过显式地和在更高的抽象级别上对反馈回路进行建模来支持开发。此外，它允许构建复杂的解决方案，其中多个反馈循环相互作用或相互作用，这是通过在运行时保持megamodel的显式和活跃以及解释它们来利用的。
2018-05-17 cs.SE
Is Three the Magic Number? An Empirical Evaluation of LLM-Based Repair Loops
Humboldt-Universität zu Berlin（柏林洪堡大学）；Korea University（高丽大学）
研究基于大语言模型的修复循环迭代限制，通过多个软件工程任务观察到收益递减模式，前几次迭代收获大，后续贡献小，还发现修复行为受工作流编排和反馈设计影响更大。
2026-07-07 cs.SE
SilGAN: Generating driving maneuvers for scenario-based software-in-the-loop testing
Volvo Group（沃尔沃集团）；Chalmers University of Technology（查尔姆斯理工大学）
汽车软件测试继续在很大程度上依赖于昂贵的现场测试来确保质量，因为基于模拟的测试等替代方法相对不成熟。作为降低对现场测试依赖的一步，我们提出了SilGAN，这是一种深度生成模型，可以简化汽车软件在环测试的规范，刺激生成和自动化。该模型使用现场车辆记录的数据进行训练。在训练时，该模型使用驾驶场景的简明规范来生成在这种场景期间可能发生的真实车辆状态转换。这种内部车辆行为的真实仿真可以用于车辆控制软件的快速、系统和廉价的测试。此外，通过提出一种有针对性的方法来搜索模型学习到的信息，我们展示了如何自动化测试目标，如代码覆盖率。我们提出的数据驱动的端到端测试管道极大地扩展了基于汽车仿真的测试的范围和可信度。这缩短了上市时间，同时有助于保持所需的质量标准。
2021-07-05 cs.LG cs.SE
Facilitating Asynchronous Participatory Design of Open Source Software: Bringing End Users into the Loop
随着开放源码软件（OSS）变得越来越成熟和流行，在适当考虑不同最终用户的可用性问题方面存在重大挑战。参与式设计，即多个利益相关者合作迭代设计，可以是解决OSS项目可用性问题的有效方法。然而，诸如以代码为中心的思维和工具支持不足等障碍往往阻止OSS团队有效地将最终用户纳入参与式设计方法。本文提出了这个问题的初步贡献，通过以用户为中心的探索（1）一套设计准则，捕捉OSS参与式设计工具的需求，（2）两个人物角色，代表OSS设计师和最终用户的特点，（3）一个低保真度的原型工具，最终用户参与OSS项目。这项工作铺平了道路，为未来的研究工具设计，最终将有助于提高OSS的可用性。
2021-02-24 cs.HC cs.SE
EndWatch: A Practical Method for Detecting Non-Termination in Real-World Software
本文提出 EndWatch，通过状态重访预言、SRC 符号推断与具体执行检查，将非终止性检测集成到 AFL 等测试工具中，在基准和真实项目上显著优于现有工具。
2023-12-06 cs.SE
AI-Augmented Closed-Loop Quality Engineering: A Reference Architecture for Continuous Software Quality Intelligence
Dimple Bajaj
提出一种AI增强的闭环参考架构，通过需求特征挖掘、风险测试优先级、缺陷预测和生产事件分析，结合有限反馈学习模型，在六个发布周期中减少缺陷泄漏、提高检测效率并缩短测试执行时间。
2026-06-07 cs.AI cs.SE
Toward Automated Virtual Electronic Control Unit (ECU) Twins for Shift-Left Automotive Software Testing
University of Applied Sciences Esslingen（埃斯林根应用科技大学）；NUVUS GmbH（NUVUS有限公司）
本研究提出一种自动化虚拟ECU双胞胎方法，通过代理驱动的工作流和反馈机制，实现早期软件测试和集成，提升测试的可重复性和安全性。
2026-02-20 cs.SE
Design Patterns for Self Adaptive Systems Engineering
自适应被提出来克服今天的软件系统的复杂性，这导致的不确定性问题。不确定性的方面包括改变系统目标、改变资源可用性和动态操作条件。反馈控制回路已被认为是工程自适应系统的重要组成部分。然而，尽管它们很重要，但仍然缺乏设计包括一个特定反馈控制回路的不同部件之间的交互以及来自不同控制回路的部件之间的交互的系统方法。大多数现有的方法要么是特定领域的，要么太抽象而没有用处。此外，多个控制回路的问题往往被忽视，因此自适应系统往往是围绕一个单一的回路设计。本文基于IBM体系结构蓝图中的MAPE-K控制环，考虑到多控制环的问题，提出了一套用于自适应软件系统建模和设计的设计模式。一个案例研究来说明所提出的设计模式的适用性。
2015-08-06 cs.SE
Human-In-the-Loop Software Development Agents
Monash University（莫纳什大学）；The University of Melbourne（墨尔本大学）；Atlassian（Atlassian公司）
本文提出并在 JIRA 中部署人在回路的 LLM 多智能体框架 HULA，让工程师在编码计划与代码生成各阶段提供反馈，评估表明其可减少简单任务的开发时间与工作量，但代码质量仍有挑战。
2025-01-10 cs.AI cs.HC cs.LG
Model Checking Embedded C Software using k-Induction and Invariants (extended version)
本文提出了一种基于归纳法的证明方法，将k-归纳法与不变量相结合，对嵌入式C软件中有界循环和无界循环进行模型检验。k-归纳算法由三种情况组成：在基本情况下，我们的目标是找到一个反例，最多有k个循环展开;在正向条件下，我们检查循环是否已经完全展开，以及安全属性P是否在k个展开内的所有状态下都成立;在归纳步骤中，我们检查每当P对k个展开成立时，它在系统的下一个展开后也成立。对于k-归纳算法的每一步，我们使用仿射约束来推断不变量（即，多面体）指定前置和后置条件。实验结果表明，我们的方法可以处理各种各样的安全特性，在典型的嵌入式软件应用程序，从电信，控制系统和医疗设备，我们证明了改进的感应算法的有效性，如果与其他方法相比。
2015-09-08 cs.LO cs.SE
Expert-in-the-Loop Systems with Cross-Domain and In-Domain Few-Shot Learning for Software Vulnerability Detection
本研究针对网络威胁下的高效软件漏洞检测需求，对比大语言模型不同提示策略并结合基于置信度的专家在环路由机制，验证了少样本提示的性能提升效果，为AI辅助漏洞检测系统部署提供基础。
2025-06-11 cs.CR cs.SE
Feedback Loops and Code Perturbations in LLM-based Software Engineering: A Case Study on a C-to-Rust Translation System
Otto von Guericke University（奥托·冯·格里克大学）；Bosch Research（博世研究）
本文研究了反馈循环、LLM选择和代码扰动对C到Rust翻译系统性能的影响，发现反馈循环可减少模型差异并提升系统鲁棒性。
2026-08-06 cs.AI cs.SE
Closing the Loop: A Software Framework for AI to Support Business Decision Making
Airbnb（爱彼迎）
本文提出一个软件框架，通过数学简化和软件设计优化，提升AI在商业闭环中的学习与迭代效率，改进因果分析并增强实验效果预测。
2026-04-27 cs.SE stat.AP
MaxMind: A Memory Loop Network to Enhance Software Productivity based on Large Language Models
National University of Defence Technology（国防科技大学）；School of Computer（计算机学院）；Southeast University（东南大学）；School of Integrated Circuits（集成电路学院）
本文提出记忆循环网络MaxMind，通过经验记忆、价值区分和知识精确分割增强RAG，并在电子表格系统中验证其可提升任务成功率与执行效率。
2024-08-07 cs.AI cs.SE
Formal-Method-Guided Vibe Coding: Closing the Verification Loop on AI-Generated Safety-Critical Software Through Model-Driven Engineering
Lancaster University（兰卡斯特大学）；Tsinghua University（清华大学）；Harbin Institute of Technology（哈尔滨工业大学）；Southwest University（西南大学）；Aarhus University（奥胡斯大学）；University of York（约克大学）
提出Forge管道，结合Vibe编码与模型驱动工程，通过多种形式化验证（Dafny、CSP、Isabelle）迭代修正LLM生成的Java代码，生成符合安全标准的验证证据。
2026-06-24 cs.FL cs.SE
Enhancing Software Engineering Through Closed-Loop Memory Optimization
William & Mary（威廉玛丽学院）；Carnegie Mellon University（卡内基梅隆大学）；OpenHands University（OpenHands大学）；University of Illinois Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
提出闭环内存优化框架，通过验证下游影响来定义内存效用，作为评估基准和优化信号，显著提升软件工程代理的成功率和效率。
2026-10-27 cs.AI cs.SE
A Design Theory for AI-Assisted Software Development Derived from Christopher Alexander's Theory of Form
Teddysoft（泰迪软件）；National Taipei University of Technology（国立台北科技大学）
针对LLM生成代码不满足需求的问题，基于亚历山大形式理论提出不匹配治理开发（MGD）方法论，通过显式表示、检测器、修复循环和人类门控回路，实现LLM代码的可靠保障。
2026-10-02 cs.SE
Software Engineering for Intelligent and Autonomous Systems: Report from the GI Dagstuhl Seminar 18343
软件系统越来越多地用于以不确定环境、不断变化的需求和意外故障为特征的应用领域;突然的系统故障会引起严重的安全性、舒适性或收入损失问题。在操作期间，这些系统可能需要处理若干不可预测的情况，包括系统性能的变化、系统工作量的突然变化和组件故障。这些情况可能导致偏离期望的系统行为，并且需要系统行为、参数或架构的动态适应。通过使用通常用软件实现的闭环控制，智能和自主软件系统可以通过识别异常情况、分析替代适应选项以及最终自适应到合适的新配置来动态地自适应，而无需任何或有限的人类参与。本报告总结了SEfIAS GI Dagstuhl研讨会期间开展的研究，该研讨会为SEAMS，ICAC/ICAC，SASO，Self-Aware Computing和AAMAS研究社区的早期职业研究人员和从业人员提供了加强互动和合作的论坛。
2019-04-03 cs.SE
Using a Feedback Loop for LLM-based Infrastructure as Code Generation
Irvington High School（欧文顿高中）；Barnard College, Columbia University（哥伦比亚大学巴纳德学院）
针对LLM代码生成对基础设施管理等周边任务影响有限的问题，研究LLM智能体利用IaC范式构建基础设施的能力，通过反馈循环返回IaC错误与警告以改进代码，发现循环有效性呈指数级下降至失效。
2024-11-28 cs.AI cs.SE
Closed-Loop Autonomous Software Development via Jira-Integrated Backlog Orchestration: A Case Study in Deterministic Control and Safety-Constrained Automation
本文提出了一种基于控制架构的闭环软件生命周期管理系统，通过七个阶段的确定性流程实现自动化，结合Jira状态合同和降级模式保障系统稳定性，展示了安全约束下的自动化效果。
2026-04-05 cs.AI cs.SE
Towards Mapping Control Theory and Software Engineering Properties using Specification Patterns
在软件工程（SE）中实现自适应的传统方法是通过反馈环。系统的目标可以被指定为针对系统模型进行验证的形式属性。另一方面，控制理论（CT）提供了一个完善的基础，设计反馈回路系统，并提供保证的基本属性，如稳定性，建立时间和稳态误差。目前，它是一个悬而未决的问题是否以及如何传统的SE方法自适应考虑CT的属性。考虑到这两个领域在表示属性方面的原则差异，提出这个问题是具有挑战性的。在本文中，我们迈出了回答这个问题的第一步。我们遵循自自底向上的的方法，为法拉利车队（F1）的灵感案例指定控制设计（在Simulink中），并提供稳定性和安全性的证据。然后将设计转换为进一步优化的代码（C）。接下来，我们定义属性，以验证控件属性在代码级别是否仍然有效。然后，我们巩固的解决方案，通过映射的属性在两个世界使用规范模式作为共同的语言，我们验证了这种映射的正确性。映射提供了一个可重用的工件来解决类似的问题。最后，我们概述了未来工作的机会，特别是完善和扩展映射，并研究它如何能够提高工程自适应系统的SE和CT工程师。
2022-05-23 cs.SE
Incremental Symbolic Bounded Model Checking of Software Using Interval Methods via Contractors
有界模型检验（BMC）对于发现程序属性冲突至关重要。对于不安全的程序，BMC可以快速找到从初始状态到违反状态的执行路径，从而反驳给定的安全属性。然而，BMC技术难以伪造包含循环的程序。BMC需要将程序循环逐步展开到绑定$k$，从而暴露属性冲突，这可能导致探索相当大的状态空间。在这里，我们描述和评估的第一个验证方法的基础上，通过承包商的区间方法，以减少域的变量表示的搜索空间。这种减少是基于建模为代表承包商约束的函数的指定属性。特别是，我们利用区间方法通过承包商增量分析程序循环变量和合同的属性保证举行修剪搜索探索的域，从而减少资源消耗积极。实验结果表明，我们所提出的方法的效率和有效性在一个大的基准集，包括$7044$验证任务，与国家的最先进的BMC工具相比。我们提出的方法可以减少内存使用高达$75$ \%，而验证$1$ \%更多的验证任务。
2022-09-21 cs.LO cs.SE
Can ChatGPT support software verification?
Carl-von-Ossietzky Universität Oldenburg（奥尔登堡卡尔·冯·奥西特齐大学）
本研究探索ChatGPT能否生成循环不变量以支持软件验证，实验表明其生成的不变量有效且有用，能增强Frama-C的验证能力，并提出结合大语言模型与验证器的方向。
2025-10-14 cs.AI cs.FL cs.LG
Bias in the Loop: Auditing LLM-as-a-Judge for Software Engineering
University of British Columbia（不列颠哥伦比亚大学）
本文研究了LLM作为评判者在代码评估中的偏见问题，通过测量优先的方法分析了代码生成、修复和测试生成任务中的评判制度，并发现提示偏见显著影响评判结果，甚至改变任务结论和模型排名。
2026-04-18 cs.AI cs.SE
Towards Demystifying and Repairing LLM-in-the-Loop Vulnerabilities
Tianjin University（天津大学）；Singapore Management University（新加坡管理大学）；University of Luxembourg（卢森堡大学）
通过构建首个LLM-in-the-loop漏洞数据集LLMCVE，分析发现LLM常作为目标或传播向量而非根因，并评估现有修复方法，揭示此类漏洞修复更具挑战性。
2026-07-03 cs.CR cs.SE
Environment-in-the-Loop: Rethinking Code Migration with LLM-based Agents
University College London（伦敦大学学院）；Nanjing University（南京大学）；Brunel University（布鲁内尔大学）；Delysium
本文提出了一种整合自动环境设置与代码迁移流程的框架，强调自动环境交互对代码迁移自动化的重要性。
2026-02-10 cs.SE
ConVer: Using Contracts and Loop Invariant Synthesis for Scalable Formal Software Verification
The University of Manchester（曼彻斯特大学）
提出一种自上而下的组合验证工具ConVer，利用大语言模型合成函数合约，并通过CEGAR-CEGIS循环迭代精炼合约，以解决大规模C程序形式化验证中的状态空间爆炸问题。
2026-05-26 cs.AI cs.SE
Discovering Software Parallelization Points Using Deep Neural Networks
Federal Rural University of Pernambuco（佛罗里达农村大学）
本研究提出基于深度学习的代码循环并行化潜力识别方法，用遗传算法生成两类代码构建数据集，训练DNN和CNN模型分类，验证了该方法的可行性，为软件优化提供新工具。
2025-10-01 cs.AI cs.DC cs.LG
From Prompt-Response to Goal-Directed Systems: The Evolution of Agentic AI Software Architecture
The Saudi Technology and Security Comprehensive Control Company "Tahakom"（沙特技术与安全综合控制公司）
本文探讨了代理AI从提示-响应到目标导向系统的架构演变，提出了生产级代理的参考架构、多代理拓扑分类及企业加固检查表，强调标准化代理循环和可审计控制机制的重要性。
2026-02-11 cs.SE
Closed-loop evaluation of LLM agents for embedded software development
Lucentia Research, Department of Software and Computing Systems, University of Alicante（阿利坎特大学软件与计算系统系卢森西亚研究）；Universitary Institute of Materials Technology (IUTM), Universitat Politècnica de València（巴伦西亚理工大学材料技术大学研究所）
本研究提出嵌入式编码智能体闭环评估基准，评估7种GPT与Qwen系列模型，发现gpt-5.4通过率最高，qwen3.5-27B为最强本地模型，表明高性能本地嵌入式编码智能体正在兴起。
2026-10-09 cs.AI cs.AR cs.LG
Sensor-Level Fault Diagnosis for Automotive Software Validation Using Large Language Models
Technische Universität Clausthal（克莱斯特塔尔工业大学）
该研究提出两阶段框架，用经4-bit低秩适配的LLM对HIL平台的汽车传感器记录做故障诊断，最小模型准确率达81.6%，适配循环可在单商用加速器运行。
2026-08-07 cs.SE
Self-sustaining Software Systems (S4): Towards Improved Interpretability and Adaptation
University of Cambridge（剑桥大学）
针对现代软件复杂性导致的可解释性与适应性不足，本文提出自维持软件系统S4，通过在所有知识源间构建知识循环来增强自主理解与动态适应能力。
2024-01-21 cs.AI cs.SE cs.SY
On Scaling Data-Driven Loop Invariant Inference
Microsoft Research, India（微软研究院（印度））；University of California Los Angeles, USA（加利福尼亚大学洛杉矶分校）
归纳不变量的自动综合是软件验证中的一个重要问题。一旦所有的不变量都被指定，软件验证就简化为验证条件的检查。虽然静态分析来推断不变量已经被研究了四十多年，但近年来出现了一系列数据驱动的不变量推断技术，这些技术从示例中猜测不变量，而不是分析程序文本。然而，这些技术已经被证明只能扩展到具有少量变量的程序。在本文中，我们研究了这些可扩展性问题，并在我们的工具绿洲中解决了这些问题，该工具绿洲提高了数据驱动的不变推理的规模，并在基准测试中优于最先进的系统。
2020-07-16 cs.LG cs.PL cs.SE
Formally expressing the semantics of observer-based fault detection software
其目的是创建可靠和可验证的故障检测软件，以检测安全关键动态系统中的突变。故障检测方法在监视和控制系统的数字计算机上以软件的形式实现。我们实现了三个基于故障检测方法的3自由度（3DOF）的实验室直升机，在软件的形式。我们研究这些方法的性能，以检测不同的故障在飞行过程中的闭环设置。所有选定的方法显示出可接受的检测性能。但是，不可能对每种可能的条件、输入和故障情况重复测试。在本文中，我们翻译成一个形式语言，以前用于软件验证和确认的故障检测性能和数学证明。我们将翻译后的属性以不可执行的注释的形式包含在软件中，这些注释可以被机器读取。因此，代码的一些高级功能属性可以通过自动软件验证工具进行验证。这证明了故障检测软件的一组有界数据，并在实践中增加了可靠性。
2013-12-03 cs.SE math.OC
Meta-Engineering Harnesses for AI-Native Software Production: A Contract-Driven Adversarial Verification Architecture with Early Deployment Report
HireNimbus
提出一种元工程框架，通过合约驱动、角色专业化AI代理和对抗性验证，实现AI原生软件的持续生产、验证与改进，并在小型服务公司的CTO即服务场景中部署17项功能，验证了其可靠性。
2026-05-25 cs.AI cs.SE
The Meta-Prompting Protocol: Orchestrating LLMs via Adversarial Feedback Loops
Zhejiang University（浙江大学）
元提示协议通过对抗反馈循环构建可编程自优化系统，解决LLM在关键任务中的确定性保证问题。
2025-12-17 cs.AI cs.CL cs.LG
Open-Source Autonomous Driving System Analysis and Multi-Disciplinary Hardware-in-the-Loop Research Paradigm with Reinforcement-Learning Testing and Large Language Models
School of Cyberspace Science and Technology, Beijing Jiaotong University（北京交通大学网络空间科学与技术学院）；School of Information Engineering, Chang’an University（长安大学信息工程学院）
本文针对开源自动驾驶系统实验记录分散问题，提出Apollo-on-Hongqi EV环境下的实车实验框架，结合大语言模型与强化学习测试，为相关研究提供可审查的实验基础。
2026-09-01 cs.RO cs.SE
A shallow dive into the depths of non-termination checking for C programs
针对现有非终止性检查工具在现实程序上效果不佳的问题，提出一种基于有界模型检查的健全高效技术，通过循环内断言与迭代展开深度检查循环状态，实验表明优于现有工具。
2024-09-04 cs.LO cs.SE
Model Based Synthesis of Control Software from System Level Formal Specifications
Sapienza University of Rome（罗马大学）
提出一种算法及工具QKS，从被控系统的形式化模型、实现规范和系统级形式化规范自动综合出满足安全性和活性要求且最坏情况执行时间与AD位数线性相关的控制软件。
2013-04-27 cs.SE cs.SY eess.SY
