Executable formal semantics for the POSIX shell
POSIX shell是一种广泛部署的、用于管理计算机系统的强大工具。shell是专家的控制面板，是配置、编译、安装、维护和部署系统的必要工具。尽管POSIX shell是一个强大的、关键的基础设施，但它仍然受到诽谤和误解。它的力量和微妙是一个危险的组合。我们为POSIX shell定义了一个正式的、机械化的、可执行的小步骤语义，我们称之为Smoosh。我们将Smoosh与其他七个旨在实现POSIX兼容性的shell（bash、dash、zsh、OSH、mksh、ksh 93和yash）进行了比较。使用三个测试套件--POSIX测试套件，Modernish测试套件和shell诊断，以及我们自己设备的测试套件--我们发现Smoosh的语义是最符合POSIX标准的。Modernish认为Smoosh的bug最少（只有一个，因为使用了dash的解析器），而且没有怪癖。为了证明我们的语义除了生成一个一致的、可执行的shell之外是有用的，我们还实现了一个符号步进器来说明shell的微妙行为。Smoosh将作为POSIX shell正式研究的基础，支持新shell、shell新工具和新shell设计的研究和开发。
2019-07-11 cs.OS cs.PL
Optimization of Executable Formal Interpreters developed in Higher-order Theorem Proving Systems
在最近的出版物中，我们提出了一种新的正式符号过程虚拟机（FSPVM）框架，该框架结合了高阶定理证明和符号执行，用于验证以太坊区块链系统中开发的智能合约的可靠性和安全性，而不会遇到围绕可重用性，一致性和自动化的标准问题。在Coq中基于通用的、可扩展的和可重用的形式存储器（GERM）框架、可扩展的和通用的形式中间程序设计语言（表示为Lolisa，其是使用广义代数数据库的Solidity程序设计语言的大子集）和用于Lolisa的对应的形式验证的解释器（表示为FEther）开发了表示为FSPVM-E的特定FSPVM。它是FSPVM-E的关键组成部分。然而，我们过去的工作表明，FEther标准开发的执行效率非常低。因此，FSPVM-E未能达到预期的验证效果。目前的工作解决这个问题，首先确定三个根本原因的执行效率低的正式解释。然后，我们建立这些原因的抽象模型，并提出相应的优化方案，以纠正所确定的条件。最后，我们将这些优化方案应用于FEther，并证明其执行效率得到了显着提高。
2018-08-26 cs.PL
Hornet Node and the Hornet DSL: A Minimal, Executable Specification for Bitcoin Consensus
针对比特币共识“代码即规范”的痛点，提出可执行声明式C++规范Hornet Node及专用DSL，实现主网快速同步，支持形式化验证与AI测试，为正式规范提供可行路径。
2025-09-24 cs.CR cs.PL cs.SE
Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
本文提出统一形式化框架，集成离散PLC语义、网络通信和连续物理行为，并应用偏序归约缓解状态爆炸，实现对PLC驱动系统的精确分析。
2025-07-21 cs.LO cs.PL
Comparative Study of Eight Formal Specifications of the Message Authenticator Algorithm
消息认证器算法（MAA）是用于计算消息认证码的第一密码函数之一。1987年至2001年期间，MAA被纳入国际标准（ISO 8730和ISO 8731-2），以确保银行交易的真实性和完整性。在1990年和1991年，NPL开发了三个正式但不可执行的MAA规范（VDM，Z和LOTOS）。从那时起，五个正式的可执行规范的MAA（在LOTOS，LNT，和长期重写系统）已被设计在INRIA格勒诺布尔。本文提供了MAA的概述，并根据常识标准（如简洁性、可读性和代码生成的效率）比较了其形式化规范。
2018-03-27 cs.CR cs.PL cs.SE
Synthesizing Formal Semantics from Executable Interpreters
本文提出利用文法和黑盒解释器，通过 CEGIS 将 CHC 语义综合分解为 SyGuS 表达式问题，并在 14 个解释器上验证，还发现并修复了正则表达式语义不一致。
2024-09-06 cs.PL
ThingTalk: An Extensible, Executable Representation Language for Task-Oriented Dialogues
Stanford University（斯坦福大学）
面向任务的会话代理依赖于语义解析器将自然语言转换为形式化表示。在本文中，我们提出的设计和基本原理的ThingTalk正式表示，以及如何设计改善了事务性面向任务的代理的发展。ThingTalk基于四个核心原则：（1）将用户请求直接表示为可执行语句，涵盖代理的所有功能，（2）正式而简洁地表示对话，以支持准确的上下文语义解析，（3）标准化类型和接口，以最大限度地提高代理之间的重用，以及（4）允许多个独立开发的代理组成单个虚拟助理。ThingTalk是作为Genie Framework的一部分开发的，它允许开发人员在给定数据库和API的情况下快速构建事务代理。我们将ThingTalk与现有的表示进行比较：SMCalFlow，SGD，TreeDST。与其他设计相比，ThingTalk设计更通用，更具成本效益。在MultiWOZ基准测试中，使用ThingTalk和相关工具进行评估，可获得79%的最新逐圈精度。
2022-03-23 cs.CL cs.PL
K-ESBMC: An Executable Formal Semantics of IEC 61131-3 Ladder Diagram for Validating Verifier Translations
The University of Manchester（曼彻斯特大学）；Federal University of Amazonas (UFAM)（亚马孙联邦大学）
研究IEC 6113-梯形图验证器翻译问题，核心方法是构建K-ESBMC可执行形式语义，主要贡献是为审核验证器翻译提供标准忠实预言机，验证翻译工具健全性，提升正确性论证从经验到形式。
2026-07-14 cs.AR cs.PL
Executable JavaScript as a Checkable Specification Language: A JS-SAM Case Study on SysMoBench
研究大语言模型用不同语言为真实系统写规范的情况，以SysMoBench为平台，通过添加JS-SAM进行控制比较，涵盖多个模型和系统，发现一致性是区分模型关键，规范契约决定保真度，最小契约有转录无语义推导，将可执行JavaScript作为规范基础作案例研究。
2026-07-16 cs.PL
MGQL: An Executable, Small-Step Semantics of GQL
University of Texas at Austin（德克萨斯大学奥斯汀分校）
MGQL是首个基于ISO/IEC 39075标准的GQL机械化小步操作语义，解决了现有形式化方法的不足，为GQL规范与机械化实现搭建桥梁，可对查询正确性进行形式化推理。
2026-08-26 cs.DB cs.PL
The While language
本文给出了一种简单的命令式程序设计语言的形式化。目标是研究和开发“动手”的程序设计语言的形式规范，即它的语法，操作语义和类型系统。为了获得该语言的可执行版本，我们在Racket中实现了它的操作语义和类型系统。
2016-04-12 cs.PL
A formally verified compiler back-end
本文描述了一个从Cminor（一种简单的命令式中间语言）到PowerPC汇编代码的编译器后端的开发和形式化验证（语义保持的证明），使用Coq证明助手对编译器进行编程并证明其正确性。这样的验证编译器是有用的，在形式化的方法应用于关键软件的认证的上下文中：编译器的验证保证了在源代码上证明的安全属性也适用于可执行的编译代码。
2009-11-14 cs.LO cs.PL
Formal Semantics of Heterogeneous CUDA-C: A Modular Approach with Applications
我们扩展了一个现成的，可执行的正式语义的C（埃里森和Rosu的K框架语义）与CUDA-C的核心功能。CUDA-C的混合CPU/GPU计算模型不仅对程序员提出了挑战，而且对形式方法的从业者也提出了挑战。我们的正式语义有助于揭示和澄清这些问题。我们证明了我们的语义生成一个工具，能够检测CUDA-C程序中的一些竞争条件和死锁的有用性。我们讨论了我们的模型的局限性，并认为它的可扩展性可以很容易地使更广泛的验证任务。
2012-11-27 cs.PL
A Formal Model of Checked C
我们提出了一个正式的模型，CMAC，方言的C，旨在加强空间内存安全。我们的模型特别注意动态大小的语义，可能空终止数组。我们在Coq中形式化了这个模型，并证明了任何空间内存安全错误都可以归咎于标记为未检查的程序部分;这是一个支持增量移植和向后兼容性的CNOC功能。虽然我们的模型的操作语义使用注释（“胖”）指针来执行空间安全，我们表明，这样的注释可以安全地删除：使用PLT Redex我们正式的可执行版本的模型和编译过程，从它到一个无类型的C类语言，并使用随机测试来验证生成的代码忠实地模拟原来的。最后，我们为Redex模型中的良好类型和几乎良好类型的术语开发了一个自定义的随机生成器，并使用它来搜索我们的模型和Clang Java实现之间的不一致。我们发现这些步骤是共同开发一种语言（CISC仍在开发中）和它的核心模型的有用方法。
2022-01-31 cs.PL cs.SE
SEMBridge: Tagless-Final Program Semantics with Weakest-Precondition and Bounded-Checking Interpretations
Oracle
提出SEMBridge框架，通过无标签最终风格统一生成可执行语义、最弱前置条件验证条件和有界检查，保持三者同步。
2026-05-29 cs.AI cs.PL
Defining Name Accessibility using Scope Graphs (Extended Edition)
针对现有类型系统缺乏名称可访问性形式化描述的问题，提出基于作用域图的语言参数化可访问性模型，在Statix中实现并验证了其正确性与访问修饰符合成能力。
2024-07-12 cs.PL
Foundational Refinement Proofs for EVM Bytecode, at the Price of Tokens
Argot Collective；National Technical University of Athens（雅典国立技术大学）
该研究构建了Lean框架EquiVM，利用前沿LLM以代币为代价，为EVM上23个真实合约生成了可复现的基础精化机器证明，实现了此前技术未达的特性组合，重塑验证框架架构。
2026-10-21 cs.PL
On the Formal Semantics of the Cognitive Middleware AWDRAT
本文的工作有两个目的：一方面，我们希望对自生成和自适应的认知中间件AWDRAT的关键组件的行为进行形式化描述，这样不仅有助于理解中间件的语义和技术细节，而且为扩展中间件以支持其他复杂的网络安全应用领域提供了机会;另一方面，形式化是我们证明关键组件行为正确性的前提，以确保中间件本身的安全性。然而，这里我们只关注中间件的核心和关键组件，即执行监视器，它是AWDRAT的“架构差异”模块的一部分。执行监视器的作用是识别目标系统的运行时观察和系统架构模型的预测之间的不一致。因此，为了实现这一目标，我们首先定义的正式（指称）的观察（运行时事件）和预测（可执行规范的系统架构模型）的语义，然后基于上述正式语义，我们正式的“执行监视器”的中间件的行为。
2014-12-14 cs.LO cs.PL
Certified Compilation of Choreographies with hacc
编程通信过程是具有挑战性的，因为它需要编写单独的程序，在执行过程中的正确时间执行兼容的发送和接收操作。把这个任务留给程序员很容易导致bug。编排编程通过为开发人员提供高级抽象来解决这一挑战，以便从全局角度编码所需的通信结构。给定一个编排，所涉及的流程的实现可以通过端点投影（EPP）自动生成。虽然编排编程可以防止通信实现中的手动错误，但编排编程框架的正确性关键取决于其复杂编译器的正确性，这促使了定理证明器中编排编程理论的形式化。在本文中，我们建立在这些形式化之一，构建一个工具链，从编排产生可执行代码。
2023-03-07 cs.PL
P4K: A Formal Semantics of P4 and Applications
可编程分组处理器和P4作为这种设备的程序设计语言已经获得了极大的兴趣，因为它们的灵活性使得能够快速开发以线速工作的各种应用。然而，这种灵活性，加上设备和网络的复杂性，增加了引入难以手动发现的细微错误的机会。更糟糕的是，这是一个bug可能造成灾难性后果的领域，但P4程序/网络的正式分析工具却缺失。我们认为，正式的分析工具必须基于一个正式的语义的目标语言，而不是在其非正式的规格说明。为此，我们提供了一个可执行的形式语义的P4语言的K框架。基于这种语义，K为P4提供了解释器和各种分析工具，包括符号模型检查器和演绎程序验证器。本文概述了我们的形式化的P4的K语义，以及我们在形式化过程中发现的几个P4语言设计问题。我们还讨论了K为P4程序员和网络管理员以及语言设计人员和编译器开发人员提供的工具所产生的一些应用，例如不可移植代码的检测，P4程序和网络的状态空间探索，使用符号执行的错误发现，数据平面验证，程序验证和翻译验证。
2018-04-04 cs.NI cs.PL
Formalism for Supporting the Development of Verifiably Safe Medical Guidelines with Statecharts
Illinois Institute of Technology（伊利诺伊理工学院）；San Diego State University（圣地亚哥州立大学）；University of Illinois at Urbana-Champaign（伊利诺伊大学厄巴纳-香槟分校）
提高患者护理的有效性和安全性是医疗网络物理系统的最终目标。虽然有许多医学最佳实践指南，但大多数手册中的现有指南难以让医务人员记住并应用于临床。此外，尽管指南已经过临床验证，但仅凭医疗专业人员的验证并不能保证医疗网络物理系统的安全性。因此，还需要进行形式化验证。本文提出了一个框架，我们开发的可验证安全的医疗指南的发展提供支持的正式语义。该框架允许计算机科学家与医疗专业人员合作，将医疗最佳实践指南转换为可执行的状态图模型，特别是Yakindu，以便医疗功能和属性可以快速原型化和验证。现有的形式化验证技术，特别是UPPAAL时间自动机，被集成到框架中，以提供形式化验证能力，以验证安全属性。然而，框架中使用/内置的一些组件，例如开源的Yakindu状态图以及从状态图到时间自动机的转换规则，没有内置的语义。这种模糊性是不可避免的，除非为框架定义了形式语义，这就是本文要介绍的。
2019-09-23 cs.CL cs.FL cs.LO
Catala: A Programming Language for the Law
法律是现代社会的基础，规范和管理公民日常生活的许多方面。通常，法律在不同的法院和司法管辖区受到解释、辩论和质疑。但在其他一些领域，法律几乎没有留下解释的空间，基本上旨在严格描述计算，决策过程或简单地说，算法。不幸的是，散文仍然是一个可悲的不足的工具的工作。缺乏形式主义为模棱两可留下了空间;法律法规的结构，许多段落和子章节分布在多个页面上，使得很难计算给定文本背后的算法的预期结果;而且，与任何其他缺乏具体说明的关键软件一样，非正式语言的使用使角落的情况无法解决。我们介绍Catala，这是一种新的程序设计语言，我们专门设计用于将成文法直接和系统地翻译成可执行的实现。Catala旨在通过一个共享的媒介将律师和程序员聚集在一起，他们可以一起理解，编辑和发展，弥合经常导致法律严重错误实施的差距。我们已经实现了一个编译器的Catala，并证明了其核心编译步骤的正确性，使用F* 证明助手。我们在几个伪装成算法的法律文本上评估Catala，特别是美国联邦所得税第121条和拜占庭式的法国家庭福利;在这样做的过程中，我们发现了官方实施中的一个错误。我们观察到，作为正式化过程的结果，使用Catala使律师和程序员之间的丰富互动，从而更好地理解最初的立法意图，同时产生一个正确的结构可执行规范可重用的更大的软件生态系统。
2021-07-02 cs.PL
Modeling and Verifying Cyber-Physical Systems with Hybrid Active Objects
网络物理系统（CPS）的正式建模很困难，因为它们提出了离散-连续动态和并发行为相结合的双重挑战。现有的CPS形式化规范和验证语言都是在其底层证明搜索技术之上设计的。它们缺乏高层次的结构要素。此外，它们不能有效地执行。这使得正式的CPS模型难以理解和验证，从而削弱了它们的可用性。相反，我们建议在一个活动对象（AO）语言设计的并发系统的简洁，直观的建模CPS模型。为此，我们扩展了AO语言ABS和混合主动对象（HAO）的运行时环境。在HAO中形式化的CPS模型和需求必须遵循某些通信模式，这些模式允许自动转换为差分动态逻辑，即顺序混合程序逻辑。验证是通过使用定理证明器KeYmaera X释放结果公式来实现的。我们证明了我们的方法与案例研究的实用性。
2019-06-13 cs.LO cs.PL cs.SY
Deriving Abstract Interpreters from Skeletal Semantics
本文提出一种基于骨架语义及其语义元语言抽象解释的方法，从编程语言形式化语义派生可执行抽象解释器，并通过小型命令式语言的值分析验证了其通用性与正确性。
2023-09-13 cs.PL
Fully Countering Trusting Trust through Diverse Double-Compiling
空军对Multics的评估和Ken Thompson的图灵奖演讲（“对信任的反思”）表明，编译器可以被颠覆，将恶意特洛伊木马插入关键软件，包括它们自己。如果这种“信任信任”攻击未被检测到，那么即使对系统源代码进行完整的分析，也无法找到正在运行的恶意代码。以前已知的反措施是远远不够的。如果这种攻击无法被反击，攻击者可以悄悄地破坏整个计算机系统，从而完全控制全球的金融、基础设施、军事和/或商业系统。本文的主要工作是利用“多样性双重编译”（DDC）技术来检测和有效地对抗信任攻击，具体表现为：（1）形式化证明DDC可以判断源代码和生成的可执行代码是否对应;（2）使用四个编译器演示DDC（小型C编译器、小型Lisp编译器、小型恶意损坏的Lisp编译器和大型工业强度C编译器GCC），以及（3）用于在各种真实世界场景中应用DDC的方法的描述。在DDC技术中，源代码被编译两次：使用可信编译器编译器的父源代码，然后使用第一次编译的结果编译推定编译器源代码。如果DDC结果与原始的被测编译器的可执行代码逐位相同，并且某些其他假设成立，则被测编译器的可执行代码与其假定的源代码相对应。
2010-04-30 cs.CR cs.PL
Governed Metaprogramming for Intelligent Systems: Reclassifying Eval as a Governed Effect
Mashin, Inc.（Mashin公司）
针对AI系统运行时动态生成可执行代码带来的权限放大问题，提出受控元编程语言设计，将程序表示视为一等值，将形式到可执行机器的转换作为受控效应，并通过形式化证明和mashinTalk DSL实现验证。
2026-05-26 cs.AI cs.PL
Rewriting Logic Semantics of a Plan Execution Language
计划执行交换语言（英语：Plan Execution Interchange Language，缩写：PLEXIL）是一种由NASA开发的同步语言，用于支持自主航天器操作。在本文中，我们提出了一个重写的逻辑语义PLEXIL在Maude，一个高性能的逻辑引擎。重写逻辑语义本身就是语言的形式解释器，可以用作PLEXIL执行程序实现的语义基准。在Maude中的实施还有一个额外的好处，即为PLEXIL设计人员和开发人员提供Maude提供的所有正式分析和验证工具。PLEXIL语义在重写逻辑中的形式化提出了一个有趣的挑战，由于语言的同步性和定义其语义的优先级规则。为了克服这个困难，我们提出了一个通用的程序，用于模拟同步集关系重写逻辑是健全的，确定性的关系，完成。我们还报告了两个问题，在设计层面上的原始PLEXIL语义确定的帮助下，在Maude的可执行规范。
2010-02-15 cs.LO cs.PL
