Feb, 2023

DSL组合的形式代数框架

HTML
PDF
TL;DR本研究讨论了一种使用代数结构来建模元语言的正式框架，以编写、组合和提供DSL抽象之间的互操作性，目的是为了验证元语言的组成性质。通过构建这个正式框架，并通过我们针对DARPA V-SPELLS计划所开发的管道，我们的论文全面讨论了此验证流程的概览。验证流程拆分为四个主要组件：第一是在Coq中提供元语言的正式模型；第二是在Coq中给出我们选择的代数结构的说明；第三，我们需要在Coq中实现我们的代数结构的具体实例，并给出Coq的证明，证明这个实现符合第二步的规范；最后，在Coq中给出元语言的正式模型是第三步实现的一个实例的证明。
发现论文，激发创造
  • 关于Smodels程序的稳定模型语义组合性的实现

    通过Gaifman-Shapiro-style模块架构和稳定模型语义来限制组合系统，提出一种正方案程序的模块化架构算法，并且取得了很好的效果，这也为实现程序性质讨论提供了理论基础和研究方法，对自动化组合和解析正规方案程序等方面都有非常重要的研究意义。

    Sep, 2008

  • 基于 Lambda 依赖的组合语义学

    介绍了一种新的正式语言， lambda依赖组合语义（lambda DCS），用于表示语义解析中的逻辑形式。lambda DCS逻辑形式通过消除变量并使存在量词隐式化，通常比lambda演算中的形式更紧凑。

    Sep, 2013

  • 不相交稳定模型的模块化方面

    研究答案集编程中的模块化问题，定义DLP函数和模块定理，介绍了DLP函数的分解方法和模块等价性概念。

    Jan, 2014

  • 有限时间范围下基于混合组合推理的反应合成

    本文提出了一种混合表示方法，利用显式和符号表示状态空间，并有效地利用它们的互补优势，从而提供了一种解决LTLf到DFA转换过程中三个必要条件的技术，从而解决合成中的瓶颈问题。

    Nov, 2019

  • 使用Anthem和Vampire验证紧凑逻辑程序

    研究逻辑程序与一阶理论之间关系的论文，将程序完备性的定义扩展到具有一种程序翻译器中输入语言子集的输入和输出程序，研究了这种情况下稳定模型和完备性之间的关系，并描述了两个软件工具，anthem 和 vampire，用于验证具有输入和输出的程序的正确性。

    Aug, 2020

  • 安全和协安全语言的一阶逻辑特征

    本文介绍了一种FO-TLO的片段SafetyFO和該兩個片段的對偶coSafetyFO，它們在經濟安全和反應綜合方面的表現完全適合於LTL可定義的經濟安全和反應綜合語言，這一结果充分填補了LTL片段的特性的一些空白。

    Sep, 2022

  • LTLf模块化理论的决定性片段（扩展版）

    本文研究了线性时间逻辑模块理论在有限轨迹上的应用，其中命题使用一阶公式替代，并且可以比较不同时间点引用的一阶变量。我们提出了一种用于LTLfMT表格的完备且有效的修剪规则，该规则在满足有限内存的抽象语义条件的任何LTLfMT公式下，通过增加新规则可以保证表格也能终止。最重要的是，这种技术使我们能够建立关于LTLfMT的多个片段可满足性的新的可判定性结果，并对已知类别给出新的可判定性证明。

    Jul, 2023

  • 利用大型语言模型发现归纳循环不变量

    本文通过使用大语言模型，探索了在自动程序验证中找到归纳循环不变量的新方法，并证明了其可以改进目前的技术水平。

    Nov, 2023

  • 增强形式定理证明：一个用于训练Coq代码AI模型的综合数据集

    该研究论文介绍了一个专门设计用于提高大型语言模型在解释和生成Coq代码方面能力的全面数据集，通过亦包含源引用和许可信息的数千个Coq源代码文件，初步实验表明使用该数据集训练的模型在Coq代码生成方面具有显著的潜力。

    Mar, 2024

  • 评估基于LLM驱动的用户意图形式化对于具备验证意识的语言

    通过符号测试规范来评估和验证音而语言中用户意图的质量与大型语言模型生成的和人工标注的 Dafny 规范数据集基本接近，但也显示了人工标注存在不完善的情况。我们的工作为程序用户意图形式化问题的建立基准和研究议程铺平了道路。

    Jun, 2024