JavaTA: A Logic-based Debugger for Java
本文提出了一种基于逻辑的Java程序调试方法。与传统的调试相比，我们提出了一种调试方法，Java程序使用逻辑查询的个人执行状态，也在历史上的执行。这些查询是通过我们早期研究中对面向对象程序错误的系统研究得出的。我们用一个逻辑数据库来表示Java程序执行过程中的显著事件，并将查询实现为逻辑程序。这种方法使我们能够回答一些有用的和有趣的查询有关的Java程序，如调用序列，在一定的结果，在一个特定的执行点的对象的状态等，我们的系统还提供了在调试会话期间组成新的查询的能力。我们相信，逻辑编程提供了一个面向对象的程序调试艺术的显着贡献。
2007-01-17 cs.PL
Profiling and Optimizing Java Streams
Java 8中添加了Stream API，以允许数据处理逻辑的声明式表达，通常是集合和数据集上的类似于map-reduce的数据转换。Stream API引入了两个关键的抽象。流是数据源中可用的元素序列，流管道包含操作（例如，map、filter、reduce），在执行时应用于流中的元素。流在Java开发人员中越来越流行，因为它们利用了函数式编程的简洁性并简化了数据处理的并行化。尽管流有很多好处，但与依赖命令式代码的数据处理相比，流可能会引入大量的开销，这主要是由额外的对象分配和回收以及虚拟方法调用的使用引起的。因此，开发人员需要研究流的运行时行为的方法，以减轻这种抽象开销并优化流处理。不幸的是，缺乏能够动态分析流的专用工具，以帮助开发人员专门定位降低应用程序性能的问题。在本文中，我们解决了流的分析和优化。我们提出了一种新的分析技术，用于测量的计算由流在过去的参考周期，我们用它来定位有问题的流与应用程序的性能产生重大影响。虽然准确性对于这一点至关重要，但插入的插装代码会导致执行额外的周期，这些周期部分包含在配置文件中。为了缓解这个问题，我们估计并补偿由插入的插装代码引起的额外周期。我们在StreamProf中实现了我们的方法，据我们所知，StreamProf是Java虚拟机（JVM）的第一个专用流分析器。与StreamProf，我们发现，周期分析是有效的，以检测有问题的流，其优化可…
2023-02-20 cs.PL
Phaedrus: Predicting Dynamic Application Behavior with Lightweight Generative Models and LLMs
Georgia Institute of Technology（佐治亚理工学院）
Phaedrus通过轻量级生成模型和大语言模型预测动态应用程序行为，实现无需执行的高效编译器优化。
2026-01-08 cs.PL cs.SE
Tuning Fuzzy Logic Programs with Symbolic Execution
模糊逻辑程序设计是一个不断发展的声明性范例，旨在将模糊逻辑集成到逻辑程序设计中。当指定一个模糊逻辑程序时，最困难的任务之一是确定每个规则的正确权重，以及最合适的模糊连接词和运算符。在本文中，我们介绍了一个符号扩展的模糊逻辑程序，其中一些参数可以是未知的，使用户可以很容易地看到他们可能的价值观的影响。此外，给定多个测试用例，可以自动计算这些参数的最合适的值。
2016-08-16 cs.LO 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
Typing constraint logic programs
本文提出了一个约束逻辑程序的参数多态和子类型的规定类型系统。这种类型的系统的目的是静态地检测编程错误。它为约束逻辑程序和模块引入了一种类型规则，同时保持了在约束域之间执行通常的转换的能力，以及由于子类型的灵活性而类型化元编程谓词的能力。主语归约的性质表达了规定类型系统与规则类型系统的一致性。执行模型：如果一个程序是“良好类型的”，那么所有从“良好类型的”目标开始的派生都是“良好类型的”。该性质是证明w.r.t.约束程序设计的抽象执行模型，它只通过约束的累积来进行，而w.r.t.一个丰富的执行模型与类型约束的替代。我们描述了我们的实现系统的类型检查和类型推断。本文报告了我们在ISO-Prolog、Sicstus Prolog的约束库和其它Prolog程序上进行类型检查的实验结果。
2004-05-27 cs.PL
Proving Differential Privacy with Shadow Execution
差分隐私的形式化验证的最新工作显示了可用性和表达性的趋势-生成复杂算法的正确性证明，同时最大限度地减少程序员的注释负担。有时，将这两者结合起来需要对程序逻辑进行重大更改：最近的一篇论文能够自动验证Report Noisy Max，但它涉及使用定制程序逻辑和验证器的复杂验证系统。在本文中，我们提出了一种新的证明技术，称为影子执行，并将其嵌入到一个名为ShadowDP的语言。ShadowDP使用影子执行来生成差分隐私的证明，只需很少的程序员注释，并且不依赖于自定义逻辑和验证器。除了验证报告Noisy Max，我们还证明了它可以验证稀疏向量的一个新变体，该变体报告了一些嘈杂的查询答案和嘈杂的阈值之间的差距。此外，ShadowDP降低了验证的复杂性：对于我们评估的所有算法，类型检查和验证总共最多需要3秒，而之前的工作在相同的算法上需要几分钟。
2019-07-01 cs.PL
A General Framework for Static Profiling of Parametric Resource Usage
传统的静态资源分析是在不执行程序的情况下估计程序的总资源使用量，本文提出了一种新的资源分析方法，其目的是对累积成本进行静态分析，即，对于节目的选定部分，发现在这些部分中的每一个中累积的资源使用的估计或界限。传统的资源分析是参数化的，因为结果可以是输入数据大小的函数。我们的静态分析也是参数化的，即，我们的累积成本估计也由输入数据大小参数化。我们的建议是基于成本中心的概念和一个程序转换，允许静态推断的功能，返回这些累积的成本取决于输入数据大小的界限，为每个成本中心的利益。这样的信息比传统的资源使用函数对软件开发者更有用，因为它允许识别应该被优化的程序的部分，因为它们对程序执行的总成本的影响更大。我们还报告了我们的实施所提出的技术使用CiaoPP程序分析框架，并提供了一些实验结果。本文件正在考虑被TPLP接受。
2016-10-17 cs.DC cs.PL
Open-Source AI-Powered Optimization in Scalene: Advancing Python Performance Profiling with DeepSeek-R1 and LLaMA 3.2
Computer Science and Engineering Bangladesh University of Engineering and Technology（孟加拉国工程与技术大学计算机科学与工程系）
本文将开源 LLM DeepSeek-R1 集成到 Python 剖析器 SCALENE 中，以替代专有 OpenAI API 自动诊断瓶颈并给出优化建议，验证其效果可与专有模型媲美。
2026-10-15 cs.PL
Automatic Verification of Iterated Separating Conjunctions using Symbolic Execution
在诸如分离逻辑之类的权限逻辑中，迭代分离合取是表示对堆位置的无界集合的访问权限的量词。与递归谓词相反，迭代分离合取并不规定它们所覆盖的位置的结构，因此不限制如何遍历和修改这些位置。这种灵活性对于验证随机存取数据结构（例如数组）和可以以多种方式遍历的数据结构（例如图形）是重要的。尽管它的有用性，没有自动程序验证原生支持迭代分离合取，他们是特别难以纳入符号执行引擎，流行的技术，为这些逻辑建立验证。在本文中，我们提出了第一个符号执行技术，以支持一般迭代分离合取。我们提出了一种新的表示符号堆和灵活的支持，量化堆位置的逻辑规范。我们的技术表现出可预测的和快速的性能，尽管在SMT级别采用量词，通过仔细控制量词实例。它与权限逻辑的其他功能兼容，如部分权限、递归谓词和抽象函数。我们的技术是实现作为一个扩展的毒蛇验证基础设施。
2016-05-06 cs.LO cs.PL
Defusing Logic Bombs in Symbolic Execution with LLM-Generated Ghost Code
Key Lab of HCST (PKU), MoE, SCS, Peking University（北京大学信息科学技术学院，复杂系统管理与控制国家重点实验室）
本文提出Gordian框架，通过LLM生成轻量级鬼代码辅助SMT求解器处理对抗性代码，提升覆盖率和效率，减少LLM使用量。
2026-09-08 cs.PL cs.SE
Design and Implementation of a Tracer Driver: Easy and Efficient Dynamic Analyses of Constraint Logic Programs
跟踪程序为用户提供有关程序执行的有用信息。在这篇文章中，我们提出了一个“跟踪驱动程序”。从单个跟踪程序开始，它提供了一个强大的前端，使多个动态分析工具能够轻松实现，同时限制了跟踪生成的开销。相关的执行事件由灵活的事件模式指定，并且可以系统地或“按需”提供大量跟踪数据。建议的跟踪驱动程序已被设计的约束逻辑编程的背景下，实验已经在GNU-Prolog。现有工具提供的执行视图可以很容易地模拟，开销可以忽略不计。实验结果表明，所描述的架构的灵活性和权力导致良好的性能。跟踪程序驱动程序开销与两个跟踪事件之间的平均时间成反比。尽管跟踪器驱动程序的原理独立于被跟踪的程序设计语言，但它最适合于高级语言，例如约束逻辑编程，其中每个被跟踪的执行事件包含许多低级执行步骤。此外，约束逻辑编程特别难以调试。当前环境没有提供所有有用的动态分析工具。他们可以从我们的跟踪驱动程序中受益匪浅，该驱动程序可以以非常低的成本集成动态分析。
2008-04-25 cs.PL cs.SE
Verification Algorithms for Automated Separation Logic Verifiers
本文系统比较了五种分离逻辑验证算法（三种现有、两种新型），在Viper基础设施上评估其性能与完备性，并提出了最大化两者的算法组合。
2024-05-27 cs.PL
CPU-less parallel execution of lambda calculus in digital logic
School of Engineering and Physical Science, University of Lincoln（林肯大学工程与物理科学学院）
本研究提出了一种无需CPU的函数式计算模型，通过将lambda演算编译为数字逻辑，实现并行执行，展示了成功执行lambda表达式的实现。
2026-02-23 cs.AR cs.DC cs.PL
Prolog Visualization System Using Logichart Diagrams
我们已经开发了一个Prolog可视化系统，旨在支持Prolog编程教育。该系统使用Logichart图来可视化Prolog程序。Logichart图被设计为可视化Prolog执行流程，并使用户能够轻松地将Prolog子句与其部分相关联。该系统具有以下功能。(1)它在Logichart图上可视地跟踪Prolog执行（目标调用、成功和失败）。(2)在Prolog程序中，通过调用逻辑外谓词（如“assertz”和“retract”）实现动态变化的实时的可视化. (3)变量替换过程在文本小部件中实时的显示。
2009-03-12 cs.HC cs.PL cs.SE
Compositional Vulnerability Detection with Insecurity Separation Logic (Extended Version)
本文提出下近似关系型程序逻辑 InsecSL，通过基于 bi-abduction 的符号执行支持交互式类 C 程序中内存安全与信息泄露的组合式、增量检测，并在两种实现上进行评估。
2023-08-21 cs.CR cs.LO cs.PL
Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus
我们调查的执行时间的语义帐户的可能性（即β步骤的数量导致的范式，如果有的话）的洗牌演算，普洛特金的调用的价值λ演算的扩展。为此，我们使用一个线性逻辑为基础的指称模型，可以被看作是一个非幂等的交集类型系统：关系语义。我们的调查的灵感来自类似的线性逻辑证明网和无类型的按名称调用的λ演算。我们首先证明了一个定性的结果：一个（可能是开放的）长期是规范化的弱减少（不减少抽象），当且仅当其解释是不空的。然后，我们表明，类型派生的大小可以用来衡量执行时间。最后，我们表明，不同的情况下，线性逻辑和呼叫的名称的λ演算演算，封闭在类型派生的定量信息不提升类型（即术语的解释）。为了在按值调用设置中获得执行时间的真正语义度量，我们推测需要对其语法和操作语义进行细化。
2019-04-23 cs.DM cs.LO cs.PL
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
本文提出结果分离逻辑（OSL），一种同时支持正确性与不正确性推理的程序逻辑，通过框架规则和新的三归结符号执行算法，实现对具有计算效应程序的局部推理，推进了分离逻辑的合成性。
2024-03-13 cs.LO cs.PL
(Co)recursion in Logic Programming: Lazy vs Eager
CoALP（英语：CoAlgebraic Logic Programming）是逻辑编程的一种方言，旨在为逻辑编程中的递归和共递归函数带来更精确的编译时和运行时终止和生产力分析。它的第二个目标是将类似于函数定理证明器的保护惰性（共）递归引入逻辑编程。在本文中，我们解释了CoALP的懒惰特性，并将其与CoLP中的循环分析和急切执行进行了比较。最后，我们概述了未来的发展方向，在逻辑编程的守护（共）递归。
2014-05-20 cs.LO cs.PL
EffiPair: Improving the Efficiency of LLM-generated Code with Differential Execution Feedback
Columbia University（哥伦比亚大学）
本文提出EffiPair框架，通过相对对比反馈机制在测试时迭代优化代码效率，减少性能反馈开销，实验证明其在代码效率提升方面优于传统方法。
2026-09-29 cs.AI cs.CL cs.LG
