Proceedings Fourth International Workshop on Rewriting Techniques for Program Transformations and Evaluation
本卷包含2017年9月8日在英国牛津举行的第四届程序转换和评估重写技术国际研讨会（WPTE 2017）的正式会议记录，并与第二届计算和演绎形式结构国际会议（FSCD 2017）有关。
2018-02-16 cs.LO cs.PL
Automating the Diagram Method to Prove Correctness of Program Transformations
我们报告的自动化技术，以证明程序转换的正确性，在高阶程序演算，这可能允许递归让绑定，因为它们发生在功能程序设计语言。如果程序转换保持了程序的观察语义，那么它就是正确的。在我们的LRSX工具中，所谓的图方法是通过结合高阶元语言上的α重命名的统一、匹配和推理来自动化的，并且通过编码来自动化归纳证明到术语重写系统的终止问题中。我们解释的技术，我们说明了使用的工具，我们报告的实验。
2019-02-22 cs.LO cs.PL
Proceedings Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation
本卷包含2016年6月23日在葡萄牙波尔图举行的第三届程序转换和评估重写技术国际研讨会（WPTE 2016）的正式会议记录，作为第一届计算和演绎形式结构国际会议（FSCD 2016）的卫星活动。该研讨会汇集了研究人员的程序转换，评估，和基于操作的程序设计语言语义，使用重写方法，以分享技术和最新发展，并交流思想，鼓励进一步激活在这一领域的研究。
2017-01-01 cs.LO cs.PL
Verification of Object-Oriented Programs: a Transformational Approach
我们表明，验证面向对象的程序，通过断言的方法，可以实现在一个简单的方式，通过利用一个语法导向的转换，从面向对象的程序递归程序。这种转换表明自然的证明规则和它的正确性，帮助我们建立健全和相对完整的证明系统。困难之一是如何在断言语言中正确处理实例变量和别名。所讨论的程序设计语言支持数组、实例变量、失败和带参数的递归方法。
2011-11-08 cs.LO cs.PL
Transformations of Logic Programs with Goals as Arguments
我们考虑逻辑编程的一个简单扩展，其中变量可以在目标上变化，目标可以是谓词的参数。在这种语言中，我们可以编写以目标为数据的逻辑程序。我们给出了实际的证据表明，利用这种能力时，转换程序，我们可以提高程序的效率。我们提出了一套程序转换规则，扩展了熟悉的展开和折叠规则，并允许我们操纵的目标出现的谓词参数的条款。为了证明这些转换规则的正确性，我们形式化地定义了我们的扩展逻辑程序设计语言的操作语义。这个语义是LD-分辨率的一个简单变体。当适当的条件得到满足时，这种语义与LD-分辨率一致，因此，用我们的扩展语言编写的程序可以由普通的Prolog系统运行。我们的转换规则，以保持操作语义和终止。
2004-02-20 cs.LO cs.PL
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 Higher-Order Abstract Syntax Approach to Verified Transformations on Functional Programs
我们描述了一种方法来验证实现的转换功能的程序，利用高阶表示的语法。在这种方法中，使用遗传Harrop公式的逻辑指定变换。一方面，这些规范直接作为实现，是Lambda Prolog语言中的程序。另一方面，它们可以用作Abella系统的输入，该系统允许我们证明关于它们的属性，从而证明关于实现的属性。我们认为，这种方法是特别有效的实现转换，分析绑定结构。我们通过在Lambda Prolog中描述对这种结构敏感的类型化闭包转换和代码提升等转换的简洁编码，并通过展示如何使用Abella证明其正确性来做到这一点。
2016-01-23 cs.LO cs.PL
Combining Logic Programs and Monadic Second Order Logics by Program Transformation
本文提出了一种基于展开/折叠变换规则的程序合成方法，该方法可用于从一个后继者的弱一元二阶理论（WS 1 S）的公式导出可终止的确定性逻辑程序。这种综合方法也可作为WS_（1 S）封闭公式的判定过程的证明方法。我们应用我们的综合方法翻译CLP（WS 1 S）程序到逻辑程序，我们也使用它作为一种证明方法来验证无限状态系统的安全性。
2003-11-27 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
Transformations of Logic Programs on Infinite Lists
我们考虑一个扩展的逻辑程序，称为ω-程序，可以用来定义谓词的无限列表。ω-程序允许我们指定反应系统的无限行为的性质，一般来说，无限事件序列的性质。ω-程序的语义是完美模型语义的扩展。我们提出了熟悉的展开/折叠规则的变体，可用于转换ω-程序。我们表明，这些新的规则是正确的，也就是说，他们的应用程序保持完美的模型语义。然后，我们概述了一个一般的方法，基于程序转换的ω-程序的性质验证。我们通过证明Buechi自动机和ω-正则语言的一些性质来展示我们基于转换的验证方法的强大功能。
2010-07-23 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
Analysis and Transformation of Constrained Horn Clauses for Program Verification
本文综述了最近的工作应用分析和转换技术，起源于约束逻辑编程（CLP）领域的问题，验证软件系统。我们提出了基于专业化的技术翻译验证问题，为不同的程序设计语言，并在一般的软件系统，到满足性问题的约束霍恩条款（CHCs），一个术语，已成为流行的验证领域，指CLP程序。然后，我们描述了静态分析技术的CHCs，可用于推断相关的程序属性，如循环不变。我们还概述了一些转换技术的基础上专业化和折叠/展开规则，这是有用的，以提高CHC可满足性工具的有效性。最后，我们讨论了应用这些技术的未来发展。
2021-08-02 cs.LO cs.PL
Proceedings of the Third International Workshop on Verification and Program Transformation
本卷包含2015年4月11日在英国伦敦举行的第三届验证和程序转换国际研讨会（VPT 2015）上发表的论文。讲习班的前两届讲习班分别于2013年在圣彼得堡（俄罗斯）和2014年在维也纳（奥地利）举行。这些论文表明，在程序转换领域中开发的方法和工具，如部分求值和折叠/展开转换，以及超级编译，可以应用于软件系统的验证。他们还展示了一些程序验证方法，如模型检验技术，抽象解释，SAT和SMT解决，自动定理证明，可以用来增强程序转换技术，从而使这些技术在实践中更强大和有用。
2015-12-06 cs.LO cs.PL cs.SE
Towards a General Framework for Formal Reasoning about Java Bytecode Transformation
程序转换引起了广泛的兴趣，因为它用于多种目的：改变程序的语义、向程序添加功能或执行优化。在本文中，我们专注于程序转换在字节码级别。由于这些转换可能会引入错误，因此我们的目标是提供一种正式的方法来验证更新并确定其正确性。提出的形式化框架定义了更新的形式语义，作为静态验证的基础，并提出了一种基于Hoare三元组和最弱前提演算的字节码转换行为推理方案
2013-07-31 cs.LO cs.PL
On Solving Word Equations via Program Transformation
本文给出了一个通过特殊化配置WE（R，E）来求解文字方程的实验，其中程序WE可以被看作是一个解释器，用来测试替换R的组合是否产生文字方程E的解。这种解释器的几个变体，当专门使用基本的展开/折叠策略时，能够确定具有重叠变量的多组单词方程的可解性。
2021-06-19 cs.LO cs.PL
Deriving sorting algorithms via abductive logic program transformation
用展开/折叠法进行逻辑程序变换，提倡通过对简单程序应用某些规则，写出正确的逻辑程序。本文主要研究如何通过逻辑程序转换和溯因推理克服子目标引入困难，从一个简单的排序算法合成有效的排序算法。
2018-10-04 cs.PL
Proving Equivalence Between Imperative and MapReduce Implementations Using Program Transformations
分布式程序通常在MapReduce、Spark和Thrill等流行的功能框架中制定，但为此类框架编写高效的算法通常是一项不平凡的任务。由于大规模运行错误算法的成本可能很高，因此非常需要验证它们的正确性。我们建议采用现有的命令式参考实现作为MapReduce实现的规范。为此，我们提出了一种新的验证方法，其中一个命令和MapReduce实现之间的等价性建立了一系列的程序转换。在本文中，我们提出了如何等价框架可以用来证明之间的等价性的PageRank算法和MapReduce变种的强制性实现。八个单独的转换步骤分别介绍和解释。
2018-03-27 cs.LO cs.PL
Inferring Program Transformations from Type Transformations for Partitioning of Ordered Sets
在本文中，我介绍了一种机制，以获得程序transformation- tions从顺序保持转换的向量类型。这项工作的目的是允许自动生成正确的建设实例的程序中的流数据处理的范例适合FPGA处理。我们表明，它是可以自动派生的实例程序的基础上结合使用foldl和地图，纯粹从类型转换的不透明的元素处理功能的组合。
2015-04-21 cs.PL
Transformational Verification of Quicksort
为约束逻辑程序开发的许多转换技术，也称为约束Horn子句（CHC），在程序验证领域中找到了新的有用的应用。在本文中，我们通过基于转换的验证方法进行了一个非平凡的案例研究。我们认为熟悉的Quicksort程序排序列表，写在一个功能性的程序设计语言，我们验证的前/后置条件，指定预期的正确性属性的功能中定义的程序。我们通过以下方式验证这些属性：（1）将它们转换为CHC，（2）通过删除所有列表出现来转换CHC，以及（3）通过使用布尔和整数的Eldarica求解器来检查转换后的CHC的可满足性。在第（2）点提到的转换需要对以前工作中提出的消除归纳定义的数据结构的算法进行扩展，因为在转换的一个阶段，我们使用在以前阶段已经证明的一些性质作为引理。
2020-08-07 cs.LO cs.PL
Proceedings Fifth International Workshop on Rewriting Techniques for Program Transformations and Evaluation
本卷包含2018年7月8日在英国牛津举行的第五届程序转换和评估重写技术国际研讨会（WPTE 2018）的正式会议记录，并与FLoC 2018和FSCD 2018相关联。WPTE的范围：重写技术对于研究程序转换、翻译和评估的正确性有很大的帮助，WPTE的目的是将研究程序转换、评估和基于操作的程序设计语言语义的研究人员聚集在一起，使用重写方法，以分享技术和最新发展，并交换想法，鼓励进一步激活这一领域的研究。WPTE范围内的主题包括程序转换，优化和翻译的正确性;证明终止，汇合和其他属性的程序转换;评估策略的正确性;程序的操作语义，基于操作的程序等效，如上下文等效和互模拟;关于转换优化能力和评估成本的推理成本模型;用于验证和定理证明目的的程序变换;具有不同形式主义的程序的翻译、模拟、等价和评估策略;用于将重写技术应用于特定程序设计语言中的程序的程序变换;用于程序反演和程序合成的程序变换;用于Haskell和重写的程序变换和评估。研究论文的选择：在研讨会上提出了六份研究论文，其中五份被接受为后续程序。每一份提交的材料都由计划委员会的三到四名成员分两到三轮进行审查，一轮用于研讨会介绍，最多两轮用于在后续程序中发表。该计划还包括Jean-Pierre Jouannaud（Polytec，Palaiseau，大巴黎，法国）关于图重写框架的邀请演讲;该演讲的摘要包含在本卷中。
2019-02-21 cs.PL
Proceedings Fifth International Workshop on Verification and Program Transformation
本卷包含第五届验证和程序转换国际研讨会（VPT 2017）的会议记录。研讨会于2017年4月29日在瑞典乌普萨拉举行，隶属于欧洲软件理论与实践联合会议（ETAPS）。VPT研讨会系列的目的是提供一个论坛，来自程序转换和程序验证领域的人们可以富有成效地交换意见，并对这两个领域之间的相互作用有更深入的了解。在研讨会上宣读了七篇论文。此外，Javier Esparza（德国慕尼黑工业大学）、Manuel Hermenegildo（西班牙马德里IMDEA软件研究所）和Alexey Khoroshilov（俄罗斯莫斯科ISPRAS Linux验证中心）也应邀进行了三次演讲。
2017-08-23 cs.LO cs.PL cs.SE
Functional Logic Program Transformations
Institut für Informatik, Kiel University（基尔大学）；University of Portland（波特兰大学）
本文探讨了函数逻辑编程在实现程序变换中的优势，通过非确定性操作与确定性方法的对比，评估了Curry语言及其中间表示FlatCurry的性能。
2026-01-19 cs.PL
A Framework for Datatype Transformation
我们研究程序演化的一个维度，即程序中数据类型声明的演化。为此，设计了一套基本的变换算子。我们涵盖了结构保持重构，但也结构扩展和减少适应。进行数据类型转换的目标程序和对数据类型转换进行编码的Meta程序都是函数程序。
2003-02-24 cs.PL
From Concurrent Programs to Simulating Sequential Programs: Correctness of a Transformation
Frama-C是一个软件分析框架，它为实现C程序的各种静态和动态分析的插件提供公共基础设施和公共行为规约语言。大多数插件不支持并发。我们提出了Conc 2Seq，一个基于程序转换的框架-C插件，能够利用现有的庞大的插件代码库，并处理并发C程序。在本文中，我们形式化和草图背后的Conc 2Seq的程序转换原则的正确性证明，并提出了一个努力实现完全机械化的形式化和证明与证明助手Coq。
2017-08-24 cs.PL
A Semantics for Approximate Program Transformations
近似程序转换是一种可以在指定的经验误差范围内改变程序语义的转换。这种转换有广泛的应用：它们可以减少计算时间，功耗和内存使用，并且在某些情况下，可以允许实现不可计算的操作。近似程序变换的正确性证明是定量的。不幸的是，与标准程序转换不同，目前还没有模块化的方法来证明近似转换本身的正确性。误差界必须证明每个转换程序单独，并必须重新证明每次修改程序或一组不同的近似应用。在本文中，我们给出了一个语义，使定量推理的一个大类的近似程序变换的本地，组合的方式。我们的语义是基于程序之间的距离的概念，它定义了一个近似变换是正确的错误界意味着什么。关键的见解是，程序之间的距离一般不能用度量空间和实数来表示。相反，我们的语义承认每个类型构造的距离的自然概念;例如，数字被用作数值数据的距离，函数被用作函数数据的距离，多态数据项被用作多态数据的距离。然后，我们将展示我们的语义如何应用于两个示例近似：用浮点数替换实数和循环穿孔。
2013-04-19 cs.PL
Towards Automatic Learning of Heuristics for Mechanical Transformations of Procedural Code
IMDEA Software Institute（IMDEA软件研究所）；Universidad Politécnica de Madrid（马德里理工大学）
下一代艾级系统的当前趋势是将各种专用（协）处理器集成到传统的超级计算机中。由于异构系统在每表面单元的瓦特和FLOPS方面的效率，向更广泛的用户开放异构平台的访问是一个需要解决的重要问题。然而，异构平台限制了应用程序的可移植性，并由于所需的编程技能而增加了开发复杂性。通过定义一个逐步的转换过程，将给定的初始代码转换为语义上等价的最终代码，但适用于特定的平台，程序转换可以帮助编程异构系统更容易。程序转换系统需要定义有效的转换策略，以解决由于在过程的每个步骤中可应用的大量转换而出现的组合问题。在本文中，我们提出了一个机器学习为基础的方法来学习算法来定义程序转换策略。我们的方法提出了一种强化学习和分类方法的新组合，以有效地解决这类系统固有的问题。初步结果表明，这种方法的适用性。
2017-01-25 cs.AI cs.PL
Horn Clauses as an Intermediate Representation for Program Analysis and Transformation
许多最近的分析传统的命令式程序开始转换程序到逻辑程序，利用现有的LP分析和简单的LP语义。我们建议在整个编译过程中使用逻辑程序作为中间程序表示。通过确保确定性和单模性的限制，逻辑程序可以很容易地转换为机器语言或其他低级语言，同时保持简单的语义，使其适合作为程序分析和转换的语言。我们提出了一个简单的LP语言，强制执行确定性和单模性，并表明它使一个方便的程序表示的分析和转换。
2015-07-21 cs.PL
Symbolic Computation via Program Transformation
符号计算是自动化程序分析的一种重要方法。大多数最先进的工具作为解释器执行符号计算，并直接维护符号数据。在本文中，我们表明，它是可行的，实际上是实用的，而不是使用基于编译器的策略。使用编译器工具，我们提出并实现了一个转换，需要一个标准的程序，并输出一个程序，执行语义等价，但部分符号，计算。转换后的程序在内部维护符号值，并直接对它们进行操作，因此程序可以由工具处理，而不支持符号操作。转换的主要动机是符号验证，但也有许多其他可能的用例，包括测试生成和concolic测试。此外，由于符号计算由程序直接处理，因此使用变换简化了工具。我们已经在LLVM位代码级别实现了转换。本文包括一个实验评估，基于显式状态的软件模型检查器作为验证后端。
2018-05-31 cs.PL
Capture-Avoiding and Hygienic Program Transformations (incl. Proofs)
根据抽象语法树的程序转换通过引入变量捕获而损害引用完整性。当在生成的程序中，变量声明意外地隐藏了变量引用的预期目标时，就会发生变量捕获。现有的转换系统要么不能保证避免变量捕获，要么损害转换的实现。我们提出了一个算法，称为名称修复，自动消除变量捕获从生成的程序系统地重命名变量。名称固定由程序的绑定结构的图形表示引导，并且需要用于转换的源语言和目标语言的名称解析算法。name-fix是通用的，适用于任何支持名称起源跟踪的转换系统中的任意转换。我们验证了名称修复的正确性，并确定一个有趣的类的转换名称修复提供卫生。我们证明了名称修复的适用性，实现捕获避免替代，内联，lambda提升，和两个特定领域的语言编译器。
2014-04-23 cs.PL
Analyzing Graph Transformation Systems through Constraint Handling Rules
图转换系统和约束处理规则是基于规则的非确定性状态转换系统。GTS以其强大的融合和程序等价性分析而闻名，为此，我们在这项工作中提供了将其应用于GTS的基础。我们给出了一个健全的和完整的嵌入GTS的可移植性，研究了一个嵌入的GTS的融合，并提供了一个程序等价性分析GTS通过嵌入。结果证实了适用的CHR为基础的程序分析嵌入在CHR的其他形式主义。
2010-06-15 cs.LO cs.PL
Reasoning about Graph Programs
GP 2是一种通过图形转换进行计算的非确定性程序设计语言。GP 2的设计目标之一是语法和语义的简单性，以促进程序的形式化推理。在本文中，我们演示了四个案例研究程序员如何证明终止和部分正确的解决方案。我们认为，GP 2的图形转换规则，连同感应程序执行的长度，提供了一个方便的框架程序验证。
2016-09-13 cs.LO cs.PL
Generating Distributed Programs from Event-B Models
分布式算法在检查它们是否满足其规范方面提出了挑战。验证技术可以扩展到处理分布式算法的安全属性的验证。在本文中，我们提出了一种方法，结合正确的建设方法和转换的形式模型（事件B）到程序（DistAlgo），以解决设计验证分布式程序。我们定义了一个子集LB（本地事件B）的事件B建模语言的事件建模的经典动作的分布式程序作为内部或本地计算，发送消息和接收消息。然后我们定义LB语言的各种元素到DistAlgo程序的转换。一般的方法包括从问题的陈述开始编程，然后逐步产生初始LB模型经过几个细化步骤后得到的LB模型。LB模型的推导在当前的文件中没有描述，已经在其他作品中得到了解决。通过一个简单的例子说明LB模型到DistAlgo程序的转换。改进过程和转换的可靠性允许人们产生正确的构造分布式程序。
2020-08-07 cs.LO cs.PL
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
Inferring Region Types via an Abstract Notion of Environment Transformation
基于区域的类型系统是各种程序分析的有力工具。我们引入了一个新的推理算法的区域类型的基础上的抽象概念的环境转换。它只分析一个方法的代码一次，即使程序中有不同区域类型的方法的多次调用。这种抽象转换的元素本质上是相等和子类型的约束，它们捕获程序的流信息。特别是，我们的工作与访问图的抽象转换的定义，以保证终止的推理算法，因为它们提供了一个有限的表示字段访问路径。
2022-09-07 cs.LO cs.PL
Effect-Dependent Transformations for Concurrent Programs
我们描述了一个指称语义的抽象效果系统的高阶，共享变量并发程序设计语言。我们证明了一些一般的基于效果的程序等价物的合理性，包括并行化方程，该方程指定了用并行组合物替换顺序组合物的充分条件。效果注释是相对于由合约指定的抽象位置而不是物理足迹，这使我们特别能够显示涉及细粒度并发数据结构（例如Michael-Scott队列）的某些转换的可靠性，这些转换允许并发访问可变数据结构的不同部分。我们的语义是基于改进的痕迹为基础的语义的一阶程序，由于布鲁克斯。通过从具体位置移动到抽象位置，并添加类型细化来捕获表达式及其并发环境的可能副作用，我们能够验证许多在未细化模型中不存在的等价性。类型的含义是使用基于游戏的逻辑关系在轨迹集上表达的。两个程序$e_1$和$e_2$是逻辑相关的，如果一个程序能够解决一个两人游戏：对于任何轨迹，结果值$v_1$在$e_1$（挑战）的语义中，玩家提出，对手可以提出一个（响应）等价的轨迹，在$e_2$的语义中，具有逻辑相关的结果值$v_2$。
2015-10-08 cs.LO cs.PL
Finite Countermodel Based Verification for Program Transformation (A Case Study)
自动程序验证和程序转换都是以程序分析为基础的。在过去的十年中，一些方法使用各种自动通用程序转换技术（部分演绎，专业化，超级编译）的计算系统的不可达性属性的验证被引入和演示。另一方面，基于语义的展开-折叠程序转换方法提出了各种各样的可达性任务，并试图解决它们，旨在改善被转换程序的语义树。这意味着可以使用一些通用的验证方法来加强程序转换技术。本文讨论了Turchin的超级编译方法中如何使用安全验证方法的有限反模型的问题。我们提取了一些超级编译子算法，试图解决可达性问题，并演示了使用外部countermodel查找器来解决一些问题。
2015-12-12 cs.PL cs.SE
Deriving program transformations by demonstration
针对特定应用程序和上下文调整转换的自动代码转换很难以可访问的方式实现。在本文中，我们提出了一种方法来建立特定于应用程序的代码转换。我们的方法是基于分析的抽象语法表示的范例的本质变化的代码之前和之后的转换被应用。这个分析需要一系列的步骤来识别变化，确定如何推广它，并将其映射到Tumego术语重写系统的术语重写规则。本文中描述的方法假设程序表示在一个语言中立的术语格式，允许工具的基础上，我们的方法被应用到程序编写的主要语言使用的计算科学家利用高性能计算系统。
2013-01-18 cs.PL
Reverse Engineering from Assembler to Formal Specifications via Program Transformations
FermaT转换系统基于达勒姆大学、德蒙福特大学和Software Migrations Ltd.过去十六年进行的研究，是一个工业强度的形式转换引擎，在程序理解和语言迁移方面有许多应用。本文是一个案例研究，它使用自动化加上手动指导的转换和抽象转换为一个非常高层次的抽象规范的IBM 370汇编代码程序。
2001-05-04 cs.PL cs.SE
Effect Handling for Composable Program Transformations in Edward2
Google（谷歌）；University of Edinburgh（爱丁堡大学）
在程序设计语言社区中，代数效果和处理程序作为一种方便的、模块化的抽象出现，用于控制计算效果。他们已经发现了几个应用程序，包括并发编程，Meta编程，以及最近的概率编程，作为Pyro的Poutines库的一部分。我们调查使用的效果处理程序作为一个轻量级的抽象实现概率程序设计语言（PPLs）。我们将Edward2的现有设计解释为效果处理机制的意外实现，并扩展该设计以支持嵌套的可组合转换。我们证明，这使得简单的复杂的模型转换和推理算法的实现。
2018-11-15 cs.LG cs.PL stat.CO
Proceedings Third Workshop on Models for Formal Analysis of Real Systems and Sixth International Workshop on Verification and Program Transformation
本卷包含MARS 2018的联合会议记录，第三次真实系统形式分析模型研讨会，以及VPT 2018，第六次验证和程序转换国际研讨会，于2018年4月20日在希腊塞萨洛尼基举行，作为ETAPS 2018的一部分，欧洲软件理论与实践联合会议。MARS强调建模而非验证。它的目的是讨论从制定正式的方法来验证和分析现实的系统中吸取的教训。例如：（1）选择哪种形式主义，为什么？(2)必须进行哪些抽象，为什么？(3)系统的重要特征是如何建模的？(4)在对系统建模时是否有任何并发症？(5)采取了哪些措施来保证模型的准确性？我们邀请了论文，提出了真实系统的完整模型，这可能会为未来的比较和分析奠定基础。研讨会的目的之一是介绍不同的建模方法，并讨论每种方法的利弊。在这次研讨会上提出的系统的替代正式描述是鼓励，这应该促进改进规范形式主义的发展。VPT旨在提供一个论坛，来自程序转换和程序验证领域的人们可以卓有成效地交换意见，并对这两个领域之间的相互作用有更深入的了解。这些互动在两个方面都是有益的。一方面，在程序转换领域开发的方法和工具，如部分演绎，部分求值，折叠/展开变换和超级编译，成功地应用于验证，特别是无限状态和参数化系统的验证。另一方面，在程序验证中开发的方法，如模型检验，抽象解释，SAT和SMT求解，自动定理证明，用于增强程序转换技术，从而使这些技术在实践中更强大和有用的。
2018-03-23 cs.FL cs.LO cs.PL
Learning Syntactic Program Transformations from Examples
UFCG（坎皮纳联邦大学）；UC Berkeley（加州大学伯克利分校）；University of Wisconsin-Madison（威斯康星大学麦迪逊分校）；University of Washington（华盛顿大学）；Microsoft（微软）；University of Colorado Boulder（科罗拉多大学博尔德分校）
IDE，如Visual Studio，自动化常见的转换，如转换和提取方法重构。然而，扩展这些转换目录是复杂且耗时的。类似的现象出现在智能辅导系统中，其中教师必须编写描述“常见错误”的繁琐代码转换，以修复类似的学生提交的编程作业。我们提出REFAZER，自动生成程序转换的技术。REFAZER建立在这样的观察基础上，即开发人员执行的代码编辑可以用作学习转换的示例。示例编辑可能共享相同的结构，但涉及不同的变量和子表达式，这些变量和子表达式必须在正确的抽象级别的转换中进行泛化。为了学习转换，REFAZER利用最先进的编程方法，使用以下关键组件：（a）用于描述程序转换的新型域特定语言（DSL），（b）用于在DSL中合成转换的域特定演绎算法，以及（c）用于对合成转换进行排名的函数。我们在两个域中实例化和评估REFAZER。首先，给出了学生用来修复不正确的编程作业提交的编辑的例子，我们学习了可以修复其他学生提交的类似错误的转换。在我们对720名学生执行的4个编程任务进行的评估中，我们的技术帮助87%的学生修复了不正确的提交。在第二个域中，我们使用开发人员对同一项目应用的重复编辑来合成程序转换，该程序转换将这些编辑应用到代码中的其他位置。在我们对来自3个C#开源项目的59个重复编辑场景进行的评估中，REFAZER在83%的情况下学习了预期的程序转换。
2016-08-31 cs.LG cs.PL cs.SE
Proceedings of the Fourth International Workshop on Verification and Program Transformation
本卷包含2016年4月2日在荷兰埃因霍温举行的第四届验证和程序转换国际研讨会（VPT 2016）上提交的论文的修订版。该研讨会是欧洲软件理论与实践联合会议（ETAPS 2016）的一项活动。VPT研讨会的目的是提供一个论坛，来自程序转换领域和程序验证领域的人们可以卓有成效地交换意见，并对这两个领域之间的相互作用有更深入的了解。最近在这些领域发表的研究论文表明，相互作用是非常有益的，实际上是双向的。在一个方向上，在程序转换领域中开发的方法和工具，例如部分演绎，部分求值，折叠/展开转换和超级编译，都已成功地应用于系统的验证，特别是无限状态和参数化系统的验证。在另一个方向，在程序验证，如模型检验，抽象解释，SAT和SMT解决，自动定理证明，已被用来增强程序转换技术，从而使这些技术在实践中更强大和有用的方法。
2016-07-06 cs.PL cs.SE
Proceedings of the First Workshop on Program Transformation for Programmability in Heterogeneous Architectures
本卷包含PROHA 2016的会议记录，这是2016年3月12日在西班牙巴塞罗那举行的第一次关于异构体系结构中可编程性的程序转换的研讨会，作为CGO 2016的附属研讨会，第14届代码生成和优化国际研讨会。开发和维护异构体系结构的高性能应用程序和库，同时保留其语义并具有合理的效率是一项耗时的任务，通常只有专家才有可能。它通常需要手动调整顺序的、与平台无关的代码以适应不同的基础设施，并保持所有这些基础设施中的更改同步。这些程序修改任务成本高且容易出错。当然，帮助并在可能的情况下自动化这种转换的工具是非常感兴趣的。然而，这样的工具可能需要显著的推理和知识处理能力，包括例如能够处理一段代码的语义的机器可理解的描述;在它们适用的上下文中执行程序变换;使用策略来标识导致最佳结果代码的变换序列;以及其他。
2016-03-10 cs.DC cs.PL cs.SE
Probabilistic Resource Analysis by Program Transformation
概率资源分析的目的是从程序输入的概率分布中推导出程序可能的资源使用的概率分布。提出了一种基于多阶段自动重写的方法来分析用C语言子集编写的程序.它生成一个概率分布的资源使用作为一个可能无法计算的表达式，然后将其转换成一个封闭的形式使用过近似表达式。我们提出的技术，概述了实施和显示系统的实验结果。
2016-12-15 cs.PL
Views, Program Transformations, and the Evolutivity Problem in a Functional Language
我们报告的经验，以支持多个视图的程序，以解决暴政的主导分解功能设置。对于表达式问题的经典例子，我们考虑Haskell中两种可能的架构。我们将展示如何使用Haskell Refactorer将一个视图转换为另一个视图，以及另一种方式。这种转换是自动化的，我们将讨论如何调整Haskell Refactorer以支持这种自动化转换。最后，我们比较我们的实施意见与一些文献。
2011-01-31 cs.PL cs.SE
A Program Transformation for Continuation Call-Based Tabled Execution
关于程序终止和降低复杂性的表式评估的优点是众所周知的--因为一些建议（特别是那些基于暂停的建议）需要大量的实施、可移植性和维护工作。这种实现的努力减少了程序转换为基础的连续调用技术，在一些效率的成本。然而，Ramesh和Cheng对这个建议的传统表述限制了表谓词和非表谓词的交错，因此不能用于任意程序。在本文中，我们提出了一个完整的翻译连续调用技术，使用传统的建议所需的运行时支持，解决了这些问题，并使之有可能执行任意tableed程序。我们目前的性能结果表明，CCall提供了一个有用的权衡，可以与国家的最先进的实现竞争。
2009-01-25 cs.PL
Evaluation of Generalizability of Neural Program Analyzers under Semantic-Preserving Transformations
University of Houston（休斯顿大学）
丰富的公开源代码库，结合神经网络的进步，使数据驱动的方法程序分析成为可能。这些方法称为神经程序分析器，使用神经网络来提取程序中的模式，用于从开发生产力到程序推理的任务。尽管神经程序分析器越来越受欢迎，但其结果的可推广程度尚不清楚。在本文中，我们使用七个语义等价的程序变换对两个流行的神经程序分析器的泛化能力进行了大规模的评估。我们的研究结果警告说，在许多情况下，神经程序分析器不能很好地概括，有时程序的文本差异可以忽略不计。这些结果为神经程序分析器中的鲁棒性量化提供了初步的基础。
2021-03-18 cs.LG cs.PL cs.SE
Program Transformation to Identify List-Based Parallel Skeletons
通过从开发人员那里抽象出并行实现的细节，并行框架被用作构建块来简化并行编程的任务。大多数现有的库都提供了框架的实现，这些框架是在平面数据类型（如列表或数组）上定义的。然而，基于Java的并行编程仍然非常具有挑战性，因为它需要对底层算法进行复杂的分析，并且经常使用低效的中间数据结构。此外，给定程序的算法结构可能与基于列表的骨架的算法结构不匹配。在本文中，我们提出了一种方法来自动转换任何给定的程序，定义在一个列表，更有可能包含基于列表的骨架的实例。这便于使用基于列表的并行骨架的现有实现来并行执行转换后的程序。此外，通过使用现有的转换称为蒸馏结合我们的方法，我们产生的转换程序，包含更少的低效的中间数据结构。
2016-07-08 cs.PL
A Simple Correctness Proof for Magic Transformation
本文给出了幻变换正确性的一个简明证明。我们相信它可以提供一个有用的例子形式推理的逻辑程序。正确性属性涉及声明性语义。然而，证明涉及源程序的操作语义（LD解析）。它的简洁性是由于应用了适当的证明方法。
2010-12-10 cs.DB cs.LO cs.PL
Dataflow Graphs as Matrices and Programming with Higher-order Matrix Elements
我们考虑两类计算，承认采取线性组合的执行运行：概率采样和广义动画的Chronlow架构。我们改进了早期的技术，几乎连续的程序转换，通过采用一个纪律的二分图连接节点通过一般的变换和节点通过线性变换，这使得它有可能开发和发展这些类的计算通过连续的程序转换的Challowlow程序。二分图的使用使我们能够表示这类的Cuplow程序作为实数矩阵，并通过这些数字的连续变化来发展和修改程序。我们开发了一个形式主义的高阶的Bastlow规划这类Bastlow图的基础上的高阶矩阵元素。我们的一些软件实验进行了简要讨论。
2016-01-06 cs.PL
Neural Architecture Search as Program Transformation Exploration
University of Edinburgh（爱丁堡大学）
提高深度神经网络（DNN）的性能对编译器和神经架构搜索（NAS）社区都很重要。编译器应用程序转换以便利用硬件并行性和存储层次结构。然而，合法性问题意味着他们未能利用神经网络的自然鲁棒性。相比之下，NAS技术通过诸如卷积的分组或检查之类的操作来改变网络，从而利用DNN的弹性。在这项工作中，我们表示这样的神经架构操作程序转换的合法性取决于一个概念的代表能力。这允许它们与现有的转换组合成统一的优化框架。这种统一使我们能够将现有的NAS操作表示为更简单的转换的组合。至关重要的是，它允许我们生成和探索新的张量卷积。我们在TVM中对组合框架进行了原型设计，并能够在不同的DNN中找到优化，从而显着减少推理时间-在大多数情况下超过3 $\times$。此外，我们的计划大大减少了NAS搜索时间。代码位于~ \href{https://github.com/jack-willturner/nas-as-program-transformation-exploration}{this https url}。
2021-02-12 cs.LG cs.PL
Source-to-source optimizing transformations of Prolog programs based on abstract interpretation
在不改变其操作语义的情况下，通过转换源代码使Prolog程序更有效，这不是一个显而易见的任务。它要求用户清楚地了解Prolog编译器是如何工作的，特别是不纯的特性（如cut）的影响。编写Prolog代码的方式-例如，从句的顺序、从句中字面意思的顺序、删减或否定的使用--都会影响其效率。此外，不同的优化技术在一起应用时可能是冗余的或冲突的，这取决于调用过程的方式-例如，插入切口并启用索引。我们提出了一个优化器，基于抽象的解释，自动执行安全的代码转换的Prolog程序的上下文中的一些类的输入调用。如果过程用关于模式、类型、共享、解决方案的数量等的附加信息来注释，则该方法更有效。因此，该方法与Mercury类似。它适用于任何Prolog程序。
2007-10-31 cs.LO cs.PL cs.SE
Unfolding for CHR programs
程序转换是一种有吸引力的技术，它可以提高运行时的效率，空间消耗，更一般地优化给定的程序。从本质上讲，它由一系列的语法程序操作，保持某种语义等价。展开是大多数程序转换系统所使用的基本操作之一，它包括用过程调用的定义替换过程调用。虽然有大量的文献转换和展开的顺序程序，很少有论文已经解决了这个问题的并发语言。本文定义了一个面向可编程逻辑程序的展开系统。我们定义了一个展开规则，证明了它的正确性，并讨论了一些条件，可以用来删除一个展开规则，同时保持程序的意义。我们还证明了，在适当的条件下，合流和终止保持上述转换。逻辑程序设计理论与实践（Theory and Practice of Logic Programming，TPLP）
2013-07-02 cs.PL
