Symbolic Synthesis of Knowledge-based Program Implementations with Synchronous Semantics
本文论述了两个同步语义（时钟和同步完美回忆）的知识为基础的程序的实现的自动合成。一种方法的合成问题的基础上使用的符号表示。该方法已被实现为模型检查器MCK的扩展。实现的合成系统的两个应用程序：泥泞的儿童难题（其中的性能相比，一个明确的状态方法，在模型检查器DEMO中实现的相关问题），和一个基于知识的程序，在一个环的过程中的动态领导选举问题。
2013-10-23 cs.LO
(Quantified) Horn Constraint Solving for Program Verification and Synthesis
我们展示了如何自动工具的验证线性和分支的时间属性的程序，多线程，和功能的程序，以及程序合成可以自然地和统一地被视为求解器的约束条件的形式（量化）霍恩条款的背景逻辑理论。这样的观点可以提供各种优势，例如。例如，在一个实施例中，约束生成（也称为证明义务的生成）和约束求解（也称为证明发现）之间的关注点的逻辑分离、跨不同验证任务的求解器的重用、以及证明设计者从低级算法关注点中解放出来，反之亦然。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2014-05-29 cs.LO
Synthesis from Knowledge-Based Specifications
在程序合成中，我们把一个规格说明转换成一个保证满足规格说明的程序。在反应系统的合成中，程序运行的环境可能表现为非确定性，例如，通过在系统的不同运行中产生不同的输入序列。为了满足规范，程序需要采取行动，以便规范在其与环境交互产生的每个计算中保持。通常，程序无法观察其环境的所有属性。在这种情况下，我们应该把一个规范转换成一个程序，它的行为只取决于可观察的计算历史。这就是所谓的不完全信息综合。在这样的设置中，希望有一个基于知识的规范，它可以指程序对环境行为的不确定性。在这项工作中，我们解决的问题与不完全信息的知识和时间的逻辑规范的综合。我们表明，该问题具有相同的最坏情况下的复杂性与完整的信息合成。
2013-07-24 cs.LO
Assume-Guarantee Synthesis for Concurrent Reactive Programs with Partial Information
程序部分的综合对于并发系统是非常有用的。然而，大多数合成方法不支持常见的设计任务，如修改单个过程而无需重新合成或验证整个系统。假设保证综合（AGS）提供了对系统部分修改的鲁棒性，但迄今为止一直局限于完美的信息设置。这意味着局部变量不能对其他过程隐藏，这使得合成结果繁琐甚至不可能实现。我们解决了这个缺点，定义AGS在部分信息设置。我们分析了在不同的设置的复杂性和可判定性，表明该问题具有很高的最坏情况下的复杂性，在许多有趣的情况下是不可判定的。基于这些观察，我们提出了一个务实的算法的基础上有界综合，并证明了它的实际适用性的几个例子。
2014-11-17 cs.LO
Algebra-based Synthesis of Loops and their Invariants (Invited Paper)
可证明正确的软件是我们软件驱动社会的关键挑战之一。形式化验证确定给定程序的正确性，而程序合成的结果是一个通过构造而正确的程序。在本文中，我们概述了我们的一些结果，这两种情况下，分析程序与循环。我们考虑的循环类可以用一个常系数线性递归方程组来建模，称为C-有限递归。首先，我们描述了一种算法方法，用于合成所有的多项式等式不变量的非确定性数值单路径循环。通过逆向工程不变量合成，我们描述了一种自动化的方法来合成程序循环满足一组给定的多项式循环不变量。我们的结果证明部分正确的程序，编译器优化和生成的代数关系的数列的应用。这是邀请在VMCAI 2021上出版的预印本。
2021-03-05 cs.LO
SynRG: Syntax Guided Synthesis of Expressions with Alternating Quantifiers
程序合成是自动生成满足给定规范的表达式的任务。程序合成技术已被用于自动生成代码中的循环不变式、合成函数摘要以及通过程序草图来帮助程序员。语法引导的综合在这一领域已经是一个成功的范例，然而，一个领域的国家的最先进的解决方案下降是推理潜在的无界数据结构，如数组，规范和解决方案可能需要量词和量词交替。我们提出了SynRG，一个合成算法的基础上限制的合成问题，以产生候选解决方案的量化在有限域，然后将这些候选解决方案推广到原来的规范的无限制域。我们报告的实验不变的合成基准和程序草图基准从Java StringUtils类，并表明我们的技术可以合成表达式的所有现有的求解器。
2020-10-12 cs.LO
Completeness of Synthesis under Realizability Assumptions using Superposition
TU Wien（维也纳工业大学）
本文研究了在可实现性假设下利用超位置进行程序合成的完备性问题，通过改进超位置演算并证明其正确性和完备性，确保能够找到满足规范的可计算程序。
2026-05-19 cs.LO
Axiomatic Synthesis of Computer Programs and Computability Theorems
我们引入了一套八个通用的推理规则，通过这些规则，具有已知属性（公理）的计算机程序被转换为具有已知属性（定理）的新程序。公理被提出来形式化数论，数据库检索和可计算性理论的一部分。结果程序演算用于生成程序，以（1）确定一个数是否是另一个数的因子。(2)列出所有收入超过经理的员工。(3)列出在自身上停止no的程序集，从而证明它是递归可重复的。众所周知的事实是，不对自己停止yes的程序集是不可递归的，这一事实被形式化为一个没有解的程序要求，即不完备公理。因此，任何可以用来生成这个程序的公理（程序）本身都是不可达到的。这样的证明形式上产生了几个额外的定理，包括（4）停机问题是不可解的。开放的问题和未来的研究进行了讨论，包括使用临时排序文件，程序计算统计数据（如计数和总和），综合的程序来解决其他著名的问题，从数论，逻辑，数据库检索和可计算性理论，应用到程序设计语言语义，和形式化的逻辑和语义悖论的不完整性结果。
2000-03-22 cs.LO
Programming-By-Example by Programming-By-Example: Synthesis of Looping Programs
程序合成近年来有了许多新的应用，这在很大程度上要归功于SyGuS的引入。然而，现有的SyGuS求解器都不支持合成递归函数。我们介绍了一个多阶段的算法，在SyGuS中的递归“loolike”程序的合成编程的例子。我们单独解决约束，并将其视为递归程序如何行为的“展开”示例，并求解广义递归解。我们的方法是模块化的，支持任何SyGuS求解器。
2021-08-19 cs.LO cs.PL
Using Program Synthesis for Program Analysis
在本文中，我们确定了一个片段的二阶逻辑与限制量化，是表现力足以捕捉众多的静态分析问题（如安全证明，错误发现，终止和非终止证明，超优化）。我们将该片段称为{ \it合成片段}。合成片段中公式的可满足性在有限域上是可判定的;具体地说，判定问题是NEXPTIME完全的。如果这个片段中的公式是可满足的，则解由从二阶变量到\emph{functions over finite domains}的满足赋值组成。为了具体地找到这些解决方案，我们合成了计算函数的\emph{programs}。我们的程序合成算法对于有限状态程序是完全的，即有限域上的每个\emph{function}都是由我们可以合成的\emph{program}计算的。因此，我们可以使用我们的合成器作为二阶逻辑合成片段的决策过程，这反过来又允许我们使用它作为许多程序分析任务的强大后端。为了显示我们的方法的易处理性，我们评估了几个静态分析问题的程序合成器。
2015-08-31 cs.LO cs.PL
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers -- Extended Version
在程序合成中，在简洁和强大的规范之间有一个众所周知的权衡：如果一个规范太冗长，它可能比程序更难写;如果它太弱，合成的程序可能不符合用户的意图。在这项工作中，我们探讨使用注释限制内存访问权限的程序合成，并表明，他们可以使规范更强大，同时保持令人惊讶的简洁。具体来说，我们增强了合成分离逻辑（SSL），一个框架，用于合成堆操作程序，只读借用的逻辑机制。我们观察到，这种简约和保守的SSL扩展在几个方面有利于合成，使其更具（a）表达性（以适度的注释开销实现更强的正确性保证），（b）有效（它产生更简洁和更易于阅读的程序），（c）高效（更快的合成），（d）鲁棒性（合成效率受搜索启发式选择的影响较小）。我们解释的直觉，并提供正式的治疗只读借用。我们证实了索赔（a）-（d）通过描述我们的量化评估的一系列标准的基准规格的各种堆操纵程序的感知合成实现。
2020-01-29 cs.LO cs.PL
Imperative Program Synthesis from Answer Set Programs
我们的研究关注的是从答案集编程规范生成命令式程序。ASP是高度声明性的，是编写规范的理想选择。此外，利用否定即失败，很容易简洁地表示组合搜索问题。我们目前正致力于从ASP程序中合成命令式程序，将否定转换为有用的计算。这开辟了一种新的方式来合成程序的可执行规范。
2019-09-19 cs.LO cs.SC
Bounded Synthesis of Reactive Programs
大多数反应系统的综合算法都集中在有限状态机的构造上，而不是实际的程序。这通常会导致结构不良、不可读的代码。在本文中，我们提出了一个有界的合成方法，自动构造，从一个给定的规范在线性时间时序逻辑（LTL），一个程序在Madhusudan的简单的命令式语言的反应程序。我们开发和比较两个主要的方法减少的综合问题的布尔约束满足问题。第一个约简是基于有界合成到双向交替自动机的推广，第二个约简是基于约束系统中程序语法的直接编码。我们报告的初步经验与原型实现，这表明直接编码优于自动机的方法。
2018-07-24 cs.FL cs.LO
Program Synthesis as Dependency Quantified Formula Modulo Theory
Indian Institute of Technology Kanpur（印度理工学院坎普尔分校）；National University of Singapore（新加坡国立大学）
给定在背景理论$\mathbb{T}$上定义的输入$X$和输出$Y$上的规范$φ(X,Y)$，程序合成的问题是设计程序$f$，使得$Y=f(X)$满足规范$φ$。在过去的十年中，语法引导合成（SyGuS）已经成为程序合成的主要方法，其中除了规范$φ$之外，最终用户还指定语法$L$以辅助底层合成引擎。本文研究了无语法综合技术的可行性，定义为$\mathbb{T}$ -约束综合的子类。我们证明了$\mathbb{T}$约束合成可以简化为DQF（$\mathbb{T}$），即，找到一个独立的量化公式模理论的证明的问题。当底层理论是位向量理论时，相应的DQF（BV）问题可以进一步简化为依赖量化布尔公式（DQBF）。我们依靠在DQBF解决的进展，设计DQBF为基础的合成器，优于特定领域的程序合成技术，从而定位DQBF作为核心表示语言的程序合成。我们的实证分析表明，$\mathbb{T}$约束合成可以实现显着更好的性能比语法指导的方法。此外，通用的DQBF求解器执行与特定领域的合成技术。
2021-05-19 cs.AI cs.LO
Informal proceedings of the 32nd International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2022)
本卷是第32届基于逻辑的程序合成和转换国际研讨会的非正式会议录（LOPSTR 2022），于2022年9月21日至23日举行，作为混合（混合）会议，（在格鲁吉亚第比利斯的Ivane Javakhishvili Tbilisi State University -TSU）和虚拟，并与第24届声明式编程原理与实践国际研讨会（PPDP 2022）共同举办，作为2022年计算逻辑秋季峰会（CLAS 2022）的一部分。
2022-07-29 cs.LO cs.PL
Pre-proceedings of the 27th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2017)
本卷是2017年10月10日至12日在比利时那慕尔举行的第27届基于逻辑的程序合成和转换国际研讨会（LOPSTR 2016）的预录，并与第19届声明式编程原理和实践国际研讨会（PPDP 2017）共同举办。在研讨会讨论后，论文将通过第二轮评审和选择的正式程序。
2017-08-31 cs.LO cs.PL
A Coq-based synthesis of Scala programs which are correct-by-construction
本文介绍了一个新的编译器，允许一个基于Coq的合成的Scala程序是“正确的建设”。一个典型的工作流程的特点是用户实现一个Coq函数程序，证明这个程序的正确性，并利用Scala-of-Coq来合成一个可以无缝集成到现有工业Scala或Java应用程序中的Scala程序。
2017-06-16 cs.LO cs.PL
Pre-proceedings of the 26th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2016)
本卷是2016年9月6日至8日在英国苏格兰爱丁堡举行的第26届基于逻辑的程序合成和转换国际研讨会（LOPSTR 2016）的预录，与第18届声明式编程原理与实践国际研讨会（PPDP 2016）和第23届静态分析研讨会（SAS 2016）位于同一地点。在研讨会讨论后，论文将通过第二轮评审和选择的正式程序。
2016-09-01 cs.LO cs.PL
LTLf Synthesis on First-Order Agent Programs in Nondeterministic Environments
RWTH Aachen University（亚琛工业大学）；Roskilde University（罗斯基勒大学）
本文研究非确定性环境中Golog智能体程序的策略合成，通过构建有限博弈舞台并采用博弈论方法，确保在满足LTLf时序规范的同时实现程序，为无界对象环境下的稳健智能体行为提供框架。
2025-03-01 cs.AI cs.LO
Towards Algorithmic Synthesis of Synchronization for Shared-Memory Concurrent Programs
我们提出了一个框架，需要一个并发程序组成的不同步的进程，随着其全球并发行为的时间规范，并自动生成一个并发程序同步，确保正确的全球行为。我们的方法支持有限状态的并发程序组成的进程，可能有本地和共享变量，可能是直线或分支程序，可能正在进行或终止，并可能有程序初始化或用户初始化的变量。规约语言是命题计算树逻辑（CTL）的扩展，其使得能够容易地对控制和数据变量的安全性和活性属性进行规约。该框架还支持在不同的抽象和粒度级别上合成同步。
2012-07-04 cs.LO cs.PL
Decidable Synthesis of Programs with Uninterpreted Functions
我们确定了一个可判定的合成问题的一类程序的无限大小的条件和迭代工作在无限的数据域。我们类中的程序使用未解释的函数和关系，并遵守最近确定的产生可判定验证的称为一致性的限制。我们制定了一个功能强大的语法限制（语法指导）的合成问题，连贯的未解释的程序，我们的问题是可判定的，确定其精确的复杂性，并研究了几个变种的问题。
2020-07-22 cs.FL cs.LO cs.PL
Pre-proceedings of the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021)
本卷构成了第31届基于逻辑的程序合成和转换国际研讨会的预录（LOPSTR 2021），于2021年9月7日至8日举行，作为混合（混合）会议，双方都亲自参加（在爱沙尼亚塔林的教师之家）和虚拟，并与第23届声明式编程的原则和实践国际研讨会（PPDP 2021）共同举办。在研讨会讨论后，论文将通过第二轮评审和选择的正式程序。
2021-08-31 cs.LO cs.PL
Program Synthesis is $Σ_3^0$-Complete
本文证明程序合成在算术层级中是 $Σ_3^0$-完备的，通过构造性编码为一阶公式并归约COF问题，首次给出其一般一阶刻画，并分析变体难度。
2024-05-27 cs.CC cs.LO cs.PL
Resource-Guided Program Synthesis
本文介绍了资源引导合成，一种用于合成既满足功能规范又满足符号资源约束的递归程序的技术。该技术是类型导向的，并依赖于一个新的类型系统，结合多态细化类型与自动摊销资源分析的潜在注释。类型系统支持有效的基于约束的类型检查，并可以表达精确的基于细化的资源边界。类型可靠性证明表明，合成程序是正确的。通过紧密集成程序探索和类型检查，合成器可以利用用户提供的资源绑定来指导搜索，急切地拒绝消耗太多资源的不完整程序。在资源引导合成器ReSyn的实现是用来评估递归数据结构操作的范围内的技术。实验表明，ReSyn合成的程序比由资源不可知的合成器生成的程序更有效。此外，使用ReSyn的合成比合成和资源分析的简单组合更快。ReSyn还能够生成对于固定输入大小具有恒定资源消耗的实现，这可用于减轻侧信道攻击。
2019-04-18 cs.LO cs.PL
Inductive Synthesis for Probabilistic Programs Reaches New Horizons
Brno University of Technology（布尔诺理工大学）；University of California, Berkeley（加州大学伯克利分校）；RWTH Aachen University（亚琛工业大学）
本文提出了一种概率程序自动综合的新方法。起点是一个程序草图，表示一个有限的家庭有限状态马尔可夫链相关，但不同的拓扑结构，和PCTL规范。该方法建立在一个新的归纳预言机，greetly产生反例（CE）违反程序，并使用它们来修剪家庭。这些CE利用的语义的家庭在其最好的和最坏的情况下的行为提供了一个演绎的oracle使用MDP抽象的界限的形式。该方法还监测合成的性能，并自适应地在归纳推理和演绎推理之间切换。我们的实验表明，新的CE建设提供了一个显着更快，更有效的修剪策略，导致加速的合成过程中广泛的基准。对于具有挑战性的问题，如分散部分可观测控制器的合成，我们减少了运行时间从一天到几分钟。
2021-01-29 cs.AI cs.LO
Liveness Verification and Synthesis: New Algorithms for Recursive Programs
我们考虑递归程序的活性验证和活性合成问题。活性验证问题（LVP）是判定给定的omega-正则语言是否包含给定的omega-上下文无关语言。活性合成问题（LSP）是计算一个策略，使得当沿着该策略进行给定的omega-上下文无关游戏时，保证导出给定omega-正则语言中的单词。这两个问题分别是EXPTIME完全问题和EXPTIME完全问题。我们的贡献是新的算法具有最佳的时间复杂度。对于LVP，我们概括了最近的拉索发现算法（也称为拉姆齐算法）从有限递归程序。对于LSP，我们概括了最近的摘要为基础的算法从有限到无限的话。Lasso查找和摘要已被证明在有限状态和有限字设置的许多实现中是有效的。
2017-01-11 cs.FL cs.LO
Program Synthesis for Non-Linear Real Arithmetic: Going Beyond Realizability
IIT Bombay（印度理工学院孟买分校）；The Institute of Mathematical Sciences, Chennai（金奈数学科学研究所）；Homi Bhabha National Institute（霍米·巴巴国立研究所）；University of California at Berkeley（加州大学伯克利分校）
研究从任意非线性实数算术规范中合成程序的问题，提出在规范不可实现时仍能输出满足规范或报告无解的程序，并给出单输出变量的完备算法和一般情况下的不完备算法。
2026-05-22 cs.LO cs.PL
GPU accelerated program synthesis: Enumerate semantics, not syntax!
University of Sussex and Montanarius Ltd（苏塞克斯大学和蒙塔纳里乌斯有限公司）；CNRS, LaBRI and Université de Bordeaux（国家科学研究中心、LaBRI和波尔多大学）；Independent Researcher（独立研究者）
本文探讨了在GPU上实现基于搜索的程序合成器，通过利用公式语义最小化数据移动和减少依赖数据的分支等GPU友好技术，使合成器能处理更大规模问题且速度远超此前基于CPU的最先进方法。
2025-04-26 cs.AI cs.LO cs.PL
Noise-aware Verification and Synthesis of Quantum Programs
Institute of Science and Technology in Austria (ISTA)（奥地利科学与技术研究所）
本文针对真实有噪声硬件上的量子程序，开发噪声感知量子霍尔逻辑，实现特定硬件量子程序的有界验证与噪声最优无循环量子程序综合，经IBM Qiskit评估，发现经典概率分支是量子编程最优的必要条件。
2026-10-21 cs.FL cs.LO cs.PL
Towards Neural-Guided Program Synthesis for Linear Temporal Logic Specifications
University of Toronto（多伦多大学）；Vector Institute（向量研究所）
综合实现逻辑规范的程序是计算机科学中的经典问题。我们研究了一种特殊类型的程序合成，其目标是合成一种策略，该策略对潜在的敌对环境做出反应，同时确保所有执行满足线性时序逻辑（LTL）规范。不幸的是，通过逻辑推理解决所谓的LTL合成的精确方法不具有规模。在这项工作中，我们铸造LTL合成作为一个优化问题。我们采用了一个神经网络学习Q函数，然后用来指导搜索，并构建程序，随后验证的正确性。我们的方法在将搜索与深度学习相结合以实现LTL合成方面是独特的。在我们的实验中，学习的Q-函数提供了有效的指导与相对较小的规格的综合问题。
2019-12-31 cs.AI cs.FL cs.GT
Are There Good Mistakes? A Theoretical Analysis of CEGIS
Intel（英特尔）；UC Berkeley（加州大学伯克利分校）
反例引导的归纳综合CEGIS是用来综合程序从候选空间的程序。当候选程序空间有限时，该方法保证终止并综合出正确的程序。但是，如果程序的候选空间是无限的，该技术可能会或可能不会终止于正确的程序。本文对反例引导的归纳综合技术进行了理论分析。我们调查的候选空间，正确的程序可以使用CEGIS合成的集合是否取决于在归纳合成中使用的反例，也就是说，是否有好的错误，这将增加合成功率。我们调查是否使用最小的反例，而不是任意的反例扩大了一组候选空间的程序，归纳合成可以成功地合成一个正确的程序。我们考虑两类反例：极小反例和历史有界反例。在CEGIS的任何迭代中使用的历史有界反例由在归纳综合的先前迭代中使用的示例所限定。我们研究在这两种情况下归纳综合的功率的相对变化。我们发现，使用最小的反例MinCEGIS的合成技术具有相同的合成功率CEGIS，但使用历史有界反例HCEGIS的合成技术具有不同的功率比CEGIS，但没有占主导地位的其他。
2014-07-21 cs.AI cs.LG cs.LO
Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction
本文研究了实时的【形】系统的安全性验证与综合问题。我们介绍实时的【形】程序，这些程序由可以执行离散和实值变量赋值的指令组成。它们足够通用，可以捕获有趣的时间系统类，如时间自动机，秒表自动机，时间（d）Petri网和混合自动机。我们提出了一种使用轨迹抽象细化的半算法来解决实时的【形】程序的可达性验证问题和参数综合问题。所有提出的算法已经实施，我们已经进行了一系列的实验，比较我们的新方法的性能，以国家的最先进的工具，在经典的可达性，鲁棒性分析和参数合成定时系统。我们表明，我们的新方法提供了解决方案，这些问题是无法解决的，目前最先进的工具。
2020-07-21 cs.FL cs.LO cs.SY
Proceedings 9th Workshop on Horn Clauses for Verification and Synthesis and 10th International Workshop on Verification and Program Transformation
这些会议记录包括在第九届验证和合成霍恩条款研讨会和第十届验证和程序转换国际研讨会上提交的选定论文，这两个研讨会都隶属于ETAPS 2022。许多感兴趣的程序验证和综合问题可以直接使用Horn子句建模，CLP和CAV社区的许多最新进展都集中在有效地解决Horn子句提出的问题上。HCVS系列研讨会旨在汇集在约束/逻辑编程社区工作的研究人员（例如，ICLP和CP），程序验证（例如，CAV、TACAS和VMCAI）和自动演绎（例如，CADE，IJCAR），关于基于Horn子句的分析、验证和综合的主题。这些团体在不同的时期从不同的角度倡导关于核查和综合的霍恩条款，组织HCVS是为了促进互动和富有成效的经验交流和整合。VPT研讨会的目的是汇集在程序验证和程序转换领域工作的研究人员。这两个领域之间有很大的潜力进行有益的互动，因为：1）一方面，在程序转换领域开发的方法和工具，如部分评估，折叠/展开转换和超级编译，都已成功应用于验证无限状态和参数化系统。2)另一方面，模型检验，抽象解释，SAT和SMT解决和自动定理证明已被用来加强程序转换技术。此外，程序转换工具的正式认证，如自动重构工具和编译器，最近吸引了相当大的兴趣，提出了重大挑战。
2022-11-19 cs.LO cs.PL cs.SC
