Static Race Detection and Mutex Safety and Liveness for Go Programs (extended version)
Go是一种流行的并发程序设计语言，这要归功于它能够有效地结合并发和系统编程。在Go程序中，许多并发错误可能是由数据竞争和通信问题引起的。在本文中，我们开发了一种基于行为类型的理论来静态检测Go程序中的数据竞争和死锁。我们首先使用Go内存模型中定义的happens-before关系，在Go程序模型上指定锁安全性、活动性和数据竞争属性。我们表示这些属性的程序中的$μ$演算模型的类型，并验证它们使用类型级别的模型检查。然后，我们扩展了框架，以考虑Go的通道，并实现了一个静态验证工具，可以检测并发错误。据我们所知，这是Go语言的第一个此类静态验证框架，统一分析了由共享内存访问和异步消息传递通信混合引起的并发错误。
2021-11-18 cs.LO cs.PL
Live, Rich, and Composable: Qualities for Programming Beyond Static Text
推动编程超越静态文本代码的努力已经寻求向编程注入多种不同的品质。一个长期公认的特性是活跃性：在程序编辑时为程序员提供关于程序动态行为的深入反馈。第二个品质，长期探索但缺乏共同的艺术术语，是丰富性：允许程序员通过特定领域的表示和交互来编辑程序，而不仅仅是通过文本。在本文中，我们映射这两个品质之间的关系，并调查过去的工作，证明他们。我们观察到，结合了活性和丰富性的系统往往是以牺牲传统编程的一个基本品质为代价的：可组合性。我们认为，通过结合活性，丰富性和可组合性，编程系统可以更好地捕捉交互式计算的全部潜力，而不会留下传统代码的表现力。
2023-03-12 cs.HC cs.PL cs.SE
Context-Bounded Verification of Liveness Properties for Multithreaded Shared-Memory Programs
我们研究的多线程，共享内存程序，其中每个线程可以产生额外的线程的活性属性的上下文有界的验证。我们的主要结果表明，上下文有界的公平终止是可判定的模型，上下文有界意味着每个派生线程可以上下文切换一个固定的常数倍。我们的证明是技术性的，因为公平终止需要推理无限多线程的组成，每个线程都有无限大的堆栈。事实上，解决相关问题的技术，主要依赖于用有限状态线程替换下推线程，是不适用的。相反，我们引入一个扩展的矢量加法系统与状态（VASS），称为VASS气球（VASSB），作为一个中间模型，它是一个独立的兴趣无限状态模型。VASSB允许标记本身就是标记（气球）。我们表明，上下文有界的公平终止减少到公平终止VASSB。我们发现后一个问题是决定性的，显示了一系列的减少：从公平终止配置可达性VASSB，并从VASS的可达性问题。对于下限，在线程运行到完成（没有上下文切换）的特殊情况下，公平终止已经被认为是非基本的。我们还表明，更简单的问题，上下文有界终止是2 EXPSPACE-完整的，匹配的复杂性限制-和技术-安全验证。此外，我们还展示了公平饥饿的相关问题，它检查一些线程是否可以沿着公平运行饥饿，在上下文有界的情况下也是可判定的。可判定性采用了从公平饥饿到公平终止的复杂还原。和公平终止一样，这个问题也是非初等的。
2020-11-12 cs.FL cs.PL
Heap Reference Analysis for Functional Programs
当前的垃圾收集器留下了大量未收集的垃圾，因为它们保守地通过程序变量的可达性来近似活性。在本文中，我们描述了一系列的静态分析，作为输入的一个程序写在一阶，渴望功能程序设计语言，并发现在每个程序点的引用对象，保证不会被使用在未来。转换过程会将此类引用设为空。如果这使得对象不可访问，则可以由垃圾收集器收集。这会导致收集更多的垃圾，从而导致更少的收集。此外，对于那些回收活动对象的垃圾收集器，它使每次收集更快。我们的方法的有趣的方面是在识别所需的分析，以解决问题和他们进行的方式。我们确定了三种不同的分析--活跃性、共享性和可访问性。在活性和共享分析中，函数定义的分析独立于调用上下文。这是通过使用一个变量来表示被分析的函数的未知上下文，并设置表示函数相对于变量的效果的约束来实现的。约束的解决方案是函数的总结，该函数相对于调用上下文被参数化，并用于分析函数调用。因此，我们在调用站点实现了上下文敏感性，而无需多次分析函数。
2007-10-08 cs.PL cs.SE
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
本文提出Trillium分离逻辑框架，通过内涵细化方法强化高阶并发与分布式分离逻辑，支持证明非平凡的安全性和活性属性，并分别实例化出Fairis和扩展Aneris以验证并发与分布式系统的活性及与TLA+模型的细化关系。
2024-08-22 cs.LO cs.PL
Reversible Lifetime Semantics for Quantum Programs
Università di Catania（卡塔尼亚大学）；Université de Rouen Normandie（诺曼底鲁昂大学）
本文提出量子程序中可逆计算的语义基础，通过寿命引导的反向计算模型，定义了语义寿命和恢复不变量，证明了嵌套作用域下的组合正确性，并展示了早期回收如何减少电路深度和限制峰值活量子比特。
2026-03-15 cs.PL quant-ph
Verifying Temporal Properties of Reactive Systems by Transformation
我们展示了如何程序转换技术可以用于验证反应系统的安全性和活性特性。特别是，我们展示了如何程序转换技术蒸馏可以用来转换反应系统指定的功能语言成一个简化的形式，随后可以分析，以验证系统的时间属性。示例系统的目的是模型互斥分析使用这些技术的安全性（互斥）和活性（非饥饿），与错误，它们包含被正确识别。
2015-12-12 cs.LO cs.PL
Lazy Pointer Analysis
流和上下文敏感的指针分析通常被认为对于大型程序来说太昂贵了;大多数工具都放松了对可伸缩性的一个或两个要求。我们制定了一个流量和上下文敏感的点，以分析，是懒惰的，在以下意义上：点的信息计算只活指针和它的传播是稀疏的（限制到活范围内的各个指针）。此外，我们的分析（a）使用强活性，有效地包括死代码消除;（b）之后从may-points-to信息计算must-points-to信息，而不是使用相互固定点;（c）在过程间分析期间使用基于值的调用字符串终止（这显著减少了调用字符串的数量）。我们在GCC-4.6.0中的分析的一个简单实现给出了SPEC 2006的分析时间和点到测量的大小。使用活性将指向信息的数量减少了一个数量级，而不损失精度。对于30 kLoC以下的所有程序，我们发现结果比gcc的分析精确得多。然而，令人惊喜的是，在这个交叉点之下，我们天真的链表实现比主要用于效率的流和上下文不敏感的分析更快。我们推测，惰性流和上下文敏感的分析可能不仅更精确，而且更有效，比目前的方法。
2011-12-21 cs.PL
Towards Fully Declarative Program Analysis via Source Code Transformation
逻辑编程的进步和越来越多的工业采用Datalog启发的方法表明，越来越需要更容易地表达强大的代码分析。声明式程序分析框架（例如，使用逻辑编程（如Datasheet），与命令式实现相比，大大简化了定义分析。然而，这些框架的声明性好处只有在解析和翻译源代码以生成事实之后才能实现。事实生成仍然是分析的非声明性先驱，其中命令式实现首先解析和解释程序结构（例如，抽象语法树和控制流图）。因此，事实生成程序仍然不透明，非专家难以理解或修改。我们提出了一个新的视角，这个分析工作流程，提出声明性的事实生成，以减轻规范和探索轻量级声明性分析。我们的方法展示了跨多种语言的完全声明式分析规范的第一次冒险。其关键思想是使用声明性语法转换将源代码直接转换为分析域中的数据库事实。然后，我们在生成的事实上重用现有的Datasheet分析，产生端到端的声明性管道。作为第一近似，我们追求语法驱动的方法，并证明了生成和使用轻量级版本的活性和调用图可达性属性的可行性。然后，我们讨论了扩展声明性事实生成，也将语义信息的可操作性。
2021-12-23 cs.PL cs.SE
Language Support for Adaptation: Intent-Driven Programming in FAST
从历史上看，程序设计语言语义集中于为程序分配精确的数学含义。这个意义是一个从程序的输入域到输出域的函数，它完全由程序的句法结构决定。这样的语义促进了便携式应用的开发，该便携式应用不注意特定硬件和软件平台的性能特性和限制（诸如最大存储器占用）。本文介绍了意图驱动编程的思想，其中程序的含义还取决于一个附带的意图规范，表示如何在执行过程中动态修改普通程序的含义，以满足意图所表达的附加属性。这些包括两种内涵属性-例如，资源使用-和扩展属性-例如，计算答案的准确性。为了证明意图驱动编程模型的价值，本文提出了一种通用意图驱动的程序设计语言--称为FAST--作为Swift的扩展实现。FAST由一个意图编译器、一个分析器、一个通用控制器接口和一个运行时模块组成，该模块支持与传统C/C++代码的互操作。与现有的自适应计算框架相比，\FAST{}支持对操作环境和意图本身的变化进行动态适应，并支持混合过程控制和基于反馈和优化的控制。
2019-07-12 cs.PL
Program Synthesis using Conflict-Driven Learning
我们提出了一种新的冲突驱动的程序合成技术，能够从过去的错误中学习。给定一个违反所需规范的虚假程序，我们的合成算法识别冲突的根本原因，并学习新的引理，可以防止类似的错误在未来。具体来说，我们引入了等价模冲突的概念，并展示了如何使用这个想法来学习有用的引理，使合成器修剪大部分的搜索空间。我们已经实现了一个通用的CDCL风格的程序合成器称为新的，并评估它在两个不同的应用领域，即数据争吵在R和函数式编程列表。我们的实验证明了冲突驱动学习的实质性好处，并表明Neo优于两个最先进的合成工具Morpheus和Deepcoder，它们分别针对这些领域。
2017-11-25 cs.PL
Data-Driven Invariant Learning for Probabilistic Programs
针对概率程序循环验证中寻找不变期望的难题，提出将其视为回归问题的数据驱动合成方法，无需模板即可学习分段连续不变式，并支持黑盒访问和子不变式学习以界定期望值。
2025-03-07 cs.PL
Event-Driven Network Programming
软件定义网络（SDN）程序必须同时描述静态转发行为和响应于事件的动态更新。事件驱动的更新是正确的关键，但由于网络中的高度并发性，很难正确实现。现有的SDN平台提供了薄弱的保证，可以打破应用程序的不变量，导致的问题，如丢包，性能下降，安全违规等，本文介绍事件驱动的一致性验证，保证保持良好定义的行为时，响应事件之间的配置转换。我们提出了网络事件结构（NES）模型的更新约束，如事件可以同时启用和事件之间的因果关系。我们定义了一个扩展的NetKAT语言与可变状态，语义有状态的程序使用NES，并讨论可证明正确的战略，实现NES在SDN。最后，我们评估我们的方法经验，证明它提供了定义良好的一致性保证，同时避免昂贵的同步和数据包缓冲。
2016-04-16 cs.PL
MyProLang - My Programming Language: A Template-Driven Automatic Natural Programming Language
现代计算机程序设计语言由复杂的语法规则支配。它们与自然语言不同;它们需要大量的手工工作和大量的学习和实践，个人才能熟练并编写正确的程序。计算机编程是一门困难、复杂、不熟悉、非自动化的学科，对每个人来说都是一门具有挑战性的学科，特别是对学生、新程序员和最终用户来说。本文提出了一种新的程序设计语言和一种基于源代码生成的计算机应用程序编写环境。它主要是一种模板驱动的自动自然命令式程序设计语言，称为MyProLang。它利用GUI模板生成专有的自然语言源代码，而不是让计算机程序员手动编写代码。MyProLang是五个元素的混合。专有的自然程序设计语言，具有简单的语法规则和表达语法;自动化模板，自动生成指令，从而最大限度地减少学习和培训时间; NLG引擎，生成自然指令;源到源编译器，分析，解析和构建可执行文件;以及人体工程学IDE，包含各种功能，其作用是简化软件开发过程。MyProLang希望让编程对所有人开放，包括学生、程序员和最终用户。从这个意义上说，任何人都可以开始系统地编程，以自动化的方式和自然语言;而不必浪费时间学习如何制定指令和安排表达式，而不必忍受不熟悉的结构和符号，也不必为语法错误而烦恼。从长远来看，这提高了软件开发的生产力、质量和上市时间。
2012-04-01 cs.PL
Data-Driven Program Completion
我们介绍程序拼接，一种编程方法，旨在自动化复制，粘贴和修改在线可用代码的常用工作流程。在这里，程序员首先编写一个“草稿”，其中混合了未完成的代码、自然语言注释和测试用例或API调用序列约束形式的正确性要求。一个程序合成器，与一个大型的，可搜索的程序片段数据库进行交互，用于自动完成草案到一个程序，满足要求。合成过程分为两个阶段。首先，合成器识别数据库中与合成任务相关的少量节目。接下来，它使用枚举搜索，系统地填充这些相关程序的表达式和语句的草案。生成的程序返回给程序员，程序员可以修改它，并可能调用额外的合成轮。我们提出了一个实现的Java程序设计语言的程序拼接。该实施使用来自开源软件库的超过350万个程序的语料库。我们的评估使用该系统在一套日常编程任务，并包括一个比较与国家的最先进的竞争方法，以及用户研究。结果表明，广泛的范围和可扩展性的程序拼接，并表明该方法可以显着提高程序员的生产力。
2017-05-25 cs.PL
ProGraML: Graph-based Deep Learning for Program Optimization and Analysis
University of Edinburgh（爱丁堡大学）；ETH Zurich（苏黎世联邦理工学院）
计算系统的复杂性不断增加，这给优化编译器带来了巨大的负担，需要更加精确和积极的优化。机器学习为构建优化启发式提供了显著的好处，但在最先进的方法实现的效果与最优启发式的性能之间仍然存在差距。缩小这一差距需要在两个关键领域进行改进：一个能够准确捕捉程序语义的表示，以及一个具有足够表达能力的模型架构，以推理这种表示。我们介绍ProGraML -程序图机器学习-一种新的基于图形的程序表示使用低级别，语言不可知，和便携式格式;和机器学习模型能够执行复杂的下游任务，这些图。ProGraML表示是一个有向属性多重图，它捕获控制、数据和调用关系，并总结指令和操作数类型和排序。消息传递神经网络通过这种结构化表示来传播信息，从而实现整个程序或每个顶点的分类任务。ProGraML提供了一种通用的程序表示，它使可学习的模型能够执行对优化至关重要的程序分析类型。为此，我们首先对一套传统的编译器分析任务：控制流可达性，支配树，数据依赖，变量活性，常见的子表达式检测我们的方法的性能进行评估。在涵盖六种源程序设计语言的25万LLVM-IR文件的基准数据集上，ProGraML的平均F1得分为94.0，明显优于最先进的方法。然后，我们将我们的方法应用到两个高层次的任务-异构设备映射和程序分类-设置新的国家的最先进的性能。
2020-03-23 cs.LG cs.PF cs.PL
The process of purely event-driven programs
使用进程代数，本文描述了纯粹的事件驱动的程序设计语言背后的过程/语义的形式化。
2018-08-24 cs.LO cs.PL
Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs
针对事件驱动多线程程序，提出Event-DPOR算法，通过扩展Optimal-DPOR并采用高效冗余检查，指数级提升SMC验证效率并避免不必要探索。
2023-07-29 cs.PL cs.SE
Data-Driven Feedback Generation for Introductory Programming Exercises
本文介绍了“搜索，对齐和修复”数据驱动的程序修复框架，以自动生成反馈的入门编程练习。与现有技术不同，我们的目标是为大型或MOOC规模的入门编程课程开发一种高效，全自动和问题不可知的技术。我们利用大量可用的学生提交在这样的设置和开发新的算法来识别类似的程序，对齐正确和不正确的程序，并通过找到最小的修复修复不正确的程序。我们已经在SARFGEN系统中实现了我们的技术，并对来自Microsoft-DEV 204.1X edX课程和Microsoft CodeHunt平台的数千名真实学生的尝试进行了评估。我们的研究结果表明，SARFGEN可以在平均两秒内为89.7%的错误学生提交生成简洁，有用的反馈。它已与Microsoft-DEV 204. 1XedX类集成并部署用于生产。
2017-11-20 cs.CY cs.PL cs.SE
Data-driven Verification of Procedural Programs with Integer Arrays
IRIF（巴黎信息研究实验室）；CNRS（法国国家科学研究中心）；Mohammed VI Polytechnic University（穆罕默德六世理工大学）
本文提出一种数据驱动方法，通过将整数数组分类问题简化为整数分类问题，综合全称量化不变量及过程前置/后置条件，用于验证操作整数数组的过程化程序，并在基准测试中展现高效性与竞争力。
2025-05-21 cs.LG cs.PL
QuCtrl-BELL: A Compiler-Driven Sub-Microsecond Feedback Control Stack for Scalable Trapped-Ion Quantum Experiments
Tsinghua University（清华大学）；Hefei National Laboratory（合肥国家实验室）；University of Science and Technology of China（中国科学技术大学）
本文提出QuCtrl-BELL，一种编译器驱动的子微秒反馈控制堆栈，用于可扩展的囚离子量子实验，通过分离控制流与硬件状态数据，解决经典控制系统的根本权衡问题，展示编译器基础设施在可扩展囚离子量子控制中的可编程性、确定性定时和模块化。
2026-05-21 cs.PL cs.SY eess.SY
A Scheme-Driven Approach to Learning Programs from Input/Output Equations
我们描述了一种方法来学习，在一个长期重写设置，从输入/输出方程的函数定义。通过限制我们自己的结构递归定义，我们得到了一个相当快的学习算法，往往产生的定义接近直觉的期望。我们提供了一个Prolog原型实现我们的方法，并指出进一步调查的开放问题。
2018-02-04 cs.AI cs.LO cs.PL
Model-Driven Engineering for Quantum Programming: A Case Study on Ground State Energy Calculation
本研究提出基于模型驱动工程的新框架，结合基于门的量子计算与量子退火方法，开发了程序自动转换映射机制，应用于变分量子本征求解器算法求解基态能量，证明了该框架的实用可行性。
2024-05-27 cs.PL cs.SE quant-ph
Verifying Asynchronous Event-Driven Programs Using Partial Abstract Transformers (Extended Manuscript)
我们解决的问题，分析异步事件驱动的程序，并发代理通过无界消息队列进行通信。这类程序的安全验证问题是不可判定的。在本文中，我们提出了一种技术，结合了有界探索的收敛性测试：如果序列的某些抽象的可达状态，增加队列界限k，收敛，我们可以证明任何属性的程序，是由抽象保存。如果抽象状态空间是有限的，则收敛是有保证的;挑战在于捕捉它发生的点k_max。我们进一步证明了如何简单的不变量制定的具体域可以用来消除虚假的抽象状态，否则会阻止序列收敛。我们已经实现了我们的技术的P程序设计语言的事件驱动程序。我们的实验表明，序列的抽象往往完全自动收敛，在困难的情况下，最小的设计师支持的形式顺序可证明的不变量，这发生在一个值的k_max足够小，让该方法在实践中取得成功。
2019-05-24 cs.FL cs.LO cs.PL
Program Language Translation Using a Grammar-Driven Tree-to-Tree Model
Harvey Mudd College（哈维穆德学院）
在程序设计语言之间进行翻译的任务与翻译自然语言的挑战不同之处在于，程序设计语言是用一组严格得多的结构和语法规则来设计的。以前的工作已经使用了树到树的编码器/解码器模型，以在翻译期间利用程序的固有树结构。然而，神经解码器默认不利用目标语言的已知语法规则。在本文中，我们描述了一个树解码器，利用知识的语言的语法规则，专门生成语法正确的程序。我们发现，这种基于语法的树到树模型优于最先进的树到树模型在两种程序设计语言之间的翻译先前使用的合成任务。
2018-07-04 cs.LG cs.PL stat.ML
Type-driven Neural Programming by Example
University of Amsterdam（阿姆斯特丹大学）
在这篇论文中，我们研究了通过例子编程（PBE），这是关于找到一个程序映射给定的输入到给定的输出。传统上，PBE在形式方法与神经方法之间存在分歧，其中形式方法通常涉及演绎技术，如SAT求解器和类型，而神经方法涉及使用相应程序对样本输入-输出进行训练，通常使用基于序列的机器学习技术，如LSTM [41]。由于这种分裂，编程类型尚未用于神经程序合成技术。我们提出了一种方法，将编程类型到PBE的神经程序合成方法。我们介绍了基于这种想法的类型化神经符号程序合成（TNSPS）方法，并在函数式编程环境中对其进行测试，以经验验证类型信息可能有助于提高有限大小数据集上神经合成器的泛化能力。我们的TNSPS模型建立在现有的神经符号程序合成（NSPS），一个基于树的神经合成器结合信息的输入-输出的例子加上当前的程序，通过进一步暴露信息的类型，这些输入-输出的例子，的语法产生式规则，以及我们希望在程序中扩展的孔。我们进一步解释了如何在我们的领域内生成数据集，该领域使用Haskell的有限子集作为合成语言。最后，我们讨论几个感兴趣的话题，可能有助于进一步采取这些想法。为了可重复性，我们公开发布代码。
2020-09-17 cs.AI cs.PL cs.SE
