paperbot · PL 论文追踪

全部论文 待读 收藏

标签：逻辑与约束编程（共 251 篇，按优先级展示前 200）

P0 Just fuzz it: solving floating-point constraints using coverage-guided fuzzing
Just fuzz it：使用覆盖率引导模糊测试求解浮点约束
提出将 SMT 公式编码为程序并用覆盖率引导模糊测试求解，特别针对浮点约束，实现 JFS 工具。
FSE Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2019匹配度 8/10引用 37逻辑与约束编程测试、调试与修复
P0 LLM-Assisted Unsatisfiability Proofs for Satisfiability Modulo Theories, Oracles, and Natural Language
面向可满足性模理论、Oracle 与自然语言的 LLM 辅助不可满足性证明
首个能为含闭盒函数调用的 SMT 公式生成不可满足性证明的求解器，借助 LLM 从自然语言文档猜想辅助引理。
OOPSLA 10(OOPSLA2)2026匹配度 8/10逻辑与约束编程机器学习与程序语言
P0 Large Language Models for Safe Minimization
面向安全最小化的大语言模型
提出 SafeMin，将 LLM 与 SMT 求解器协同用于不可行字符串约束系统的安全最小化与 MUS 计算。
ICSE 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)2025匹配度 8/10机器学习与程序语言逻辑与约束编程
P1 Solving Floating-Point Constraints with Continuous Optimization
使用连续优化求解浮点约束
提出基于数学优化的 SMT 浮点约束求解器 Grater，求解数量媲美最强求解器且速度快一个数量级以上。
PLDI 9(PLDI)2025匹配度 7/10引用 2逻辑与约束编程
P1 Testing Deep Learning Libraries via Neurosymbolic Constraint Learning
通过神经符号约束学习测试深度学习库
提出神经符号约束学习技术 Centaur，从种子输入学习 DL API 约束，用 SMT 生成有效多样测试并发现新缺陷。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 7/10引用 1测试、调试与修复机器学习与程序语言逻辑与约束编程
P1 Interval constraint-based mutation testing of numerical specifications
面向数值规约的基于区间约束的变异测试
提出 Magneto，用区间约束满足自动生成数值规约的测试与 oracle，检测浮点代码的精度、鲁棒性与功能缺陷。
ISSTA Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis2021匹配度 7/10引用 1测试、调试与修复逻辑与约束编程
P1 Speeding up SMT Solving via Compiler Optimization
通过编译器优化加速 SMT 求解
提出 SLOT，将 SMT 实例翻译为 LLVM IR 并复用编译器优化进行化简，从而实现求解器无关的 SMT 加速。
FSE Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2023匹配度 6/10引用 14逻辑与约束编程编译与代码生成
P1 Fast bit-vector satisfiability
快速位向量可满足性
利用一阶公式中的区间与数据依赖信息加速 eager SMT 求解中的位向量可满足性判定。
ISSTA Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis2020匹配度 6/10引用 14逻辑与约束编程
P1 Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
不可行低维线性规划的最大共识浮点解：以凸包为中间表示
提出以凸包为中间表示求解不可行低维线性规划，生成满足最多约束的浮点解，加速正确舍入数学库多项式生成。
PLDI 8(PLDI)2024匹配度 6/10引用 3逻辑与约束编程
P1 Scalable Floating-Point Satisfiability via Staged Optimization
通过分阶段优化的可扩展浮点可满足性求解
提出 StageSAT，用三阶段逐步提升精度的数值优化求解浮点可满足性，兼顾可扩展性与可靠性。
PLDI 10(PLDI)2026匹配度 6/10逻辑与约束编程
P1 Better Together: Unifying Datalog and Equality Saturation
合则更强：统一 Datalog 与等式饱和
egglog 将 Datalog 与等式饱和（EqSat）统一为定点推理系统，兼具增量执行、同余闭包与项抽取能力。
PLDI 7(PLDI)2023匹配度 5/10引用 36逻辑与约束编程定理证明与证明工程
P1 Safe and sound program analysis with Flix
用 Flix 进行安全且可靠的程序分析
提出用 Flix 语言实现静态分析，从语言层面保障不动点计算安全终止且分析结果可靠。
ISSTA Proceedings of the 27th ACM SIGSOFT International Symposium on Software Testing and Analysis2018匹配度 5/10引用 17程序分析与抽象解释逻辑与约束编程
P1 Parasol: efficient parallel synthesis of large model spaces
Parasol：大规模模型空间的高效并行合成
Parasol 利用无监督学习指导模型空间均衡分区并并行合成，显著加速大规模形式化模型空间探索。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 5/10引用 4逻辑与约束编程机器学习与程序语言
P1 Translation Titans, Reasoning Challenges: Satisfiability-Aided Language Models for Detecting Conflicting Requirements
翻译巨人、推理挑战：可满足性辅助的语言模型用于检测冲突需求
提出 SAT-LLM，将 SMT 求解器与 LLM 协同，用于检测软件需求冲突，实验优于纯 LLM 方法。
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 5/10引用 2机器学习与程序语言逻辑与约束编程
P1 A Constraint Solving Approach to Parikh Images of Regular Languages
正则语言 Parikh 像的约束求解方法
将正则语言 Parikh 像推理转化为约束求解问题，提出 PC* 演算与工具 Catra，避免显式构造积自动机并显著加速字符串约束求解。
OOPSLA 8(OOPSLA1)2024匹配度 5/10引用 2逻辑与约束编程逻辑与自动机
P1 Probabilistic Inference for Datalog with Correlated Inputs
带相关输入的概率 Datalog 推断
提出 Praline，扩展 Datalog 以在输入事实相关时进行精确概率推断，并用 δ-exact 算法高效求出紧的概率界。
OOPSLA 9(OOPSLA2)2025匹配度 5/10引用 1逻辑与约束编程量子与概率编程
P1 Automated Debugging of Datalog Programs
Datalog 程序的自动化调试
将派生事实视为测试用例、证明树视为执行谱，把 SBFL 迁移到 Datalog，实现无需人工交互的故障规则定位。
OOPSLA 10(OOPSLA2)2026匹配度 5/10测试、调试与修复逻辑与约束编程
P1 Breaking the Dependency Chaos: A Constraint-Driven Python Dependency Resolution Strategy with Selective LLM Imputation
打破依赖混乱：一种约束驱动的 Python 依赖解析策略与选择性 LLM 填补
用 Z3 约束求解替代纯 LLM 版本猜测，仅对缺失元数据选择性调用 LLM，将 Python 依赖解析成功率从 54.8% 提升至 83.6%。
FSE Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering2026匹配度 5/10逻辑与约束编程机器学习与程序语言
P1 SMTgazer: Learning to Schedule SMT Algorithms via Bayesian Optimization
SMTgazer：通过贝叶斯优化学习调度 SMT 算法
将 SMT 求解器调度建模为超参数优化，用贝叶斯优化与集成代理实现多求解器序列组合。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 5/10逻辑与约束编程机器学习与程序语言
P1 Inference of Properties from Requirements and Automation of Their Formal Verification
从需求推断性质并自动化其形式验证
提出用 SML 元模型表达示例数据，并改进 ILP 自动推断性质，以降低形式验证中规约与证明的人工交互。
ASE 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE)2019匹配度 5/10程序验证逻辑与约束编程
P1 Solvable Tuple Patterns and Their Applications to Program Verification
可解元组模式及其在程序验证中的应用
提出可从少量正样本高效推断的（合取）可解元组模式，并用于 CHC 求解器验证递归数据结构程序。
PLDI 10(PLDI)2026匹配度 5/10程序验证逻辑与约束编程
P1 Flix: A Design for Language-Integrated Datalog
Flix：一种语言集成 Datalog 的设计
提出 Flix 中语言集成 Datalog 的设计，使 Datalog 程序可模块化、多态、类型化地复用于程序分析等任务。
OOPSLA 9(OOPSLA2)2025匹配度 5/10逻辑与约束编程语言设计与特性
P2 RustHorn: CHC-based Verification for Rust Programs
RustHorn：基于 CHC 的 Rust 程序验证
提出将带指针与动态内存的 Rust 程序归约为 CHC 的新方法，利用权限保证消除指针和内存状态，并证明可靠性与完备性。
TOPLAS 43(4)2021匹配度 4/10引用 52程序验证逻辑与约束编程
P2 Metamorphic testing of Datalog engines
Datalog 引擎的蜕变测试
提出首个针对 Datalog 引擎的蜕变测试方法，在三个成熟引擎中发现 13 个此前未知的查询错误。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 4/10引用 24测试、调试与修复逻辑与约束编程
P2 Lifting Datalog-based analyses to software product lines
将基于 Datalog 的分析提升到软件产品线
研究 Datalog 推理的 lifting 理论，并在 Soufflé 引擎中实现，将分析从单个产品提升到整个产品线。
FSE Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2019匹配度 4/10引用 20程序分析与抽象解释逻辑与约束编程
P2 Control flow-guided SMT solving for program verification
控制流引导的 SMT 求解用于程序验证
提出在 SMT 求解中利用程序控制流知识剪枝搜索空间，显著提升程序验证效率。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 4/10引用 18程序验证逻辑与约束编程
P2 Quantitative Policy Repair for Access Control on the Cloud
云上访问控制的定量策略修复
提出基于SMT与模型计数的定量符号分析，自动修复过度宽松的访问控制策略。
ISSTA Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis2023匹配度 4/10引用 14安全与隐私逻辑与约束编程
P2 Semantic Debugging
语义调试
提出自动推断程序失败原因与条件的语义调试技术，并实现 AVICENNA 原型。
FSE Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2023匹配度 4/10引用 14测试、调试与修复逻辑与约束编程
P2 Type and interval aware array constraint solving for symbolic execution
面向符号执行的类型与区间感知数组约束求解
提出类型与区间感知公理生成及ILP预检，加速符号执行中的数组约束求解。
ISSTA Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis2021匹配度 4/10引用 14逻辑与约束编程程序验证
P2 Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration
通过基于语法的枚举验证 SMT 求解器的正确性与性能
提出 ET，通过将 SMT 理论语法编译为代数数据类型并借助 FEAT 枚举，系统测试 SMT 求解器的正确性与性能。
OOPSLA 8(OOPSLA2)2024匹配度 4/10引用 13测试、调试与修复逻辑与约束编程
P2 PARTI: a multi-interval theory solver for symbolic execution
PARTI：面向符号执行的多区间理论求解器
提出多区间理论求解器 PARTI，加速符号执行中特定结构的数组与位向量查询，非该结构时回退完整求解器。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 4/10引用 12程序分析与抽象解释逻辑与约束编程
P2 Subformula Caching for Model Counting and Quantitative Program Analysis
用于模型计数与定量程序分析的子公式缓存
提出子公式缓存框架并集成到模型计数求解器，利用跨约束共享的子公式显著加速定量程序分析。
ASE 2019 34th IEEE/ACM International Conference on Automated Software Engineering (ASE)2019匹配度 4/10引用 11逻辑与约束编程程序分析与抽象解释
P2 Dependency-Aware Metamorphic Testing of Datalog Engines
Datalog 引擎的依赖感知变形测试
提出依赖感知的变形测试方法，用于发现 Datalog 引擎返回错误结果的查询缺陷。
ISSTA Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis2023匹配度 4/10引用 10逻辑与约束编程测试、调试与修复
P2 Flan: An Expressive and Efficient Datalog Compiler for Program Analysis
Flan：面向程序分析的高表达力高效 Datalog 编译器
提出嵌入 Scala 的 Datalog 编译器 Flan，用多阶段编程生成专用代码，兼顾表达力与性能。
POPL 8(POPL)2024匹配度 4/10引用 9逻辑与约束编程编译与代码生成
P2 Sibyl: Improving Software Engineering Tools with SMT Selection
Sibyl：通过 SMT 求解器选择改进软件工程工具
提出基于图神经网络的 SMT 求解器自动选择器 Sibyl，显著加速多种软件工程工具中的 SMT 查询求解。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 4/10引用 8机器学习与程序语言逻辑与约束编程
P2 When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic
当少即是多：弱算术理论中的后承发现
提出弱公理化乘法的非线性算术理论及后承发现算法，用于生成循环不变式并证明程序安全性质。
POPL 7(POPL)2023匹配度 4/10引用 8程序验证逻辑与约束编程
P2 Diver: Oracle-Guided SMT Solver Testing with Unrestricted Random Mutations
Diver：基于预言引导和无限制随机变异的 SMT 求解器测试
提出 Diver，以预言引导的无限制随机变异测试 SMT 求解器，发现 25 个新缺陷，其中 21 个关键。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 4/10引用 7测试、调试与修复逻辑与约束编程
P2 An evolutionary approach for analyzing Alloy specifications
一种分析 Alloy 规范的演化方法
提出 EvoAlloy，将遗传算法引入 Alloy，在保持可靠性的前提下放宽完备性，以扩展可处理规范规模。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 4/10引用 7程序验证逻辑与约束编程
P2 Datalog-Based Language-Agnostic Change Impact Analysis for Microservices
基于 Datalog 的微服务语言无关变更影响分析
提出 MICROSCOPE，用 Datalog 规则统一建模多语言微服务代码与配置，以识别受变更影响的接口。
ICSE 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)2025匹配度 4/10引用 6程序分析与抽象解释逻辑与约束编程
P2 Demystifying Template-Based Invariant Generation for Bit-Vector Programs
揭秘面向位向量程序的基于模板的不变式生成
系统实验揭示位向量程序中模板不变式生成的模板与求解器影响，并证明其可处理现有方法难处理的基准。
ASE 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)2023匹配度 4/10引用 6程序验证逻辑与约束编程
P2 Consistent Scene Graph Generation by Constraint Optimization
基于约束优化的一致场景图生成
提出一种约束优化后处理，保证场景图满足一致性约束并提升生成准确率。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 4/10引用 6逻辑与约束编程机器学习与程序语言
P2 A Flexible Proof Format for SAT Solver-Elaborator Communication
用于 SAT 求解器-精化器通信的灵活证明格式
提出 FRAT 证明格式与工具链，显著降低 UNSAT SAT 证明精化为 LRAT 的时间与内存开销。
LMCS vol.Volume 18, Issue 22022匹配度 4/10引用 6逻辑与约束编程定理证明与证明工程
P2 Lobster: A GPU-Accelerated Framework for Neurosymbolic Programming
Lobster：面向神经符号编程的 GPU 加速框架
提出 Lobster，将基于 Datalog 的神经符号程序编译到 GPU，实现端到端加速与可扩展推理。
ASPLOS Proceedings of the 31st ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 12025匹配度 4/10引用 5机器学习与程序语言逻辑与约束编程编译与代码生成
P2 Making Formulog Fast: An Argument for Unconventional Datalog Evaluation
让 Formulog 变快：为非常规 Datalog 求值辩护
提出 eager evaluation，替代半朴素 Datalog 求值，大幅加速 Formulog 的 SMT 静态分析。
OOPSLA 8(OOPSLA2)2024匹配度 4/10引用 5逻辑与约束编程程序分析与抽象解释
P2 Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming
基于整数线性规划的单源单目标交错 Dyck 可达性
提出用路径表达式与整数线性规划求解单源单目标 InterDyck 可达性，避免传统汇总边并显著加速。
POPL 7(POPL)2023匹配度 4/10引用 5程序分析与抽象解释逻辑与约束编程
P2 Optimizing Datalog for the GPU
面向 GPU 的 Datalog 优化
提出 GPUlog：基于哈希索引有序数组 HISA 的 GPU Datalog 引擎，实现关系代数内核并显著加速递归推理。
ASPLOS Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 12025匹配度 4/10引用 4逻辑与约束编程语言与体系结构
P2 Relational Abstractions Based on Labeled Union-Find
基于带标签并查集的关系抽象
提出带标签并查集，并基于它构造可高效表示关系约束的抽象域，用于程序分析与 SMT 求解。
PLDI 9(PLDI)2025匹配度 4/10引用 3程序分析与抽象解释逻辑与约束编程
P2 Interactive Debugging of Datalog Programs
Datalog 程序的交互式调试
提出基于自顶向下小步操作语义的 Datalog 交互式调试器，支持 step-into/step-over，并适配 Soufflé 与 IncA。
OOPSLA 7(OOPSLA2)2023匹配度 4/10引用 3逻辑与约束编程形式语义编程环境与开发者工具
P2 Dis/Equality Graphs
不相等/相等图（Dis/Equality Graphs）
首次形式化直接支持不等式的 e-graph，证明其比等式嵌入编码更高效，并在 egg 中实现验证。
POPL 9(POPL)2025匹配度 4/10引用 2逻辑与约束编程定理证明与证明工程
P2 Programming by Navigation
导航式编程（Programming by Navigation）
提出导航式编程合成问题，保证规约细化中所有且仅有有效下一步，并高效求解。
PLDI 9(PLDI)2025匹配度 4/10引用 2程序合成逻辑与约束编程
P2 Finding Cross-Rule Optimization Bugs in Datalog Engines
发现 Datalog 引擎中的跨规则优化缺陷
提出增量规则求值方法 IRE，通过对比优化程序与禁用跨规则优化的参考程序，自动检测 Datalog 引擎的优化缺陷。
OOPSLA 8(OOPSLA1)2024匹配度 4/10引用 2逻辑与约束编程测试、调试与修复
P2 SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
SMT 理论套利：使用有界理论近似无界约束
提出理论套利，将无界 SMT 约束转为有界约束以大幅加速求解。
PLDI 8(PLDI)2024匹配度 4/10引用 1逻辑与约束编程程序分析与抽象解释
P2 Validating Optimizing SMT Solvers via Cross-Theory Approximation
通过跨理论近似验证优化 SMT 求解器
提出跨理论近似方法并实现 Iris，通过理论间最优解一致性检测 OMT 求解器缺陷。
OOPSLA 10(OOPSLA2)2026匹配度 4/10逻辑与约束编程测试、调试与修复
P2 Real-to-Sim Generation: Synthesizing Scenario Programs from Real-World Data via Constraint Solving
实到仿生成：通过约束求解从真实世界数据合成场景程序
提出 R2SGEN 框架，以解耦 SMT 约束求解从真实世界数据合成结构化场景程序，克服组合爆炸并优于 LLM 基线。
OOPSLA 10(OOPSLA2)2026匹配度 4/10程序合成逻辑与约束编程
P2 Generator Solving for Symbolic Execution
面向符号执行的生成器求解
提出「生成器求解」：不求解单个解，而是求解可反复调用、持续产出新测试输入的生成器，以提升符号执行效率。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 4/10测试、调试与修复逻辑与约束编程
P2 PSMT: Satisfiability Modulo Theories Meets Probability Distribution
PSMT：当可满足性模理论遇到概率分布
提出 PSMT 问题与 Prob-MCSAT 算法，将概率分布引入 SMT 求解，使解呈现合理的分布趋势。
ASE 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)2023匹配度 4/10逻辑与约束编程量子与概率编程
P2 Horntinuum: Autonomous Testing using Constrained Horn Clauses
Horntinuum：使用约束 Horn 子句的自主测试
提出 Horntinuum，用约束 Horn 子句（CHC）驱动自主测试，实现测试的自动生成或引导。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 4/10测试、调试与修复逻辑与约束编程
P2 SymMC: approximate model enumeration and counting using symmetry information for Alloy specifications
SymMC：利用对称信息对 Alloy 规约进行近似模型枚举与计数
提出 SymMC，借助对称信息对 Alloy 规约做近似模型枚举与计数。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 4/10逻辑与约束编程
P2 Orax: A Feedback-Driven Framework for Efficiently Solving Satisfiability Modulo Theories and Oracles
Orax：一个反馈驱动的框架，用于高效求解可满足性模理论与预言机问题
提出反馈驱动的 Orax 框架，在 SMT 求解器与 oracle 处理器间闭环反馈 oracle 映射信息，高效求解 SMTO 问题。
OOPSLA 9(OOPSLA1)2025匹配度 4/10逻辑与约束编程
P2 Gigahorse: Thorough, Declarative Decompilation of Smart Contracts
Gigahorse：智能合约的彻底、声明式反编译
提出 Gigahorse 工具链，以声明式逻辑规范将 EVM 字节码反编译为高层三地址 IR，支持智能合约分析。
ICSE 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE)2019匹配度 3/10引用 166编译与代码生成逻辑与约束编程
P2 Efficient sampling of SAT solutions for testing
面向测试的 SAT 解高效采样
提出 QuickSampler，以少量 SAT 求解器调用高效生成大量满足约束的解，用于测试。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 3/10引用 106逻辑与约束编程测试、调试与修复
P2 A graph solver for the automated generation of consistent domain-specific models
面向一致性领域特定模型自动生成的图求解器
提出直接在图结构上求解的图求解器，用于自动生成满足元模型与良构约束的大规模一致领域模型。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 3/10引用 53领域特定语言与建模逻辑与约束编程
P2 Syntax-guided synthesis of Datalog programs
语法引导的 Datalog 程序合成
提出 ALPS，利用语法引导剪枝从输入输出示例合成 Datalog 程序。
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 3/10引用 51程序合成逻辑与约束编程
P2 Provenance-guided synthesis of Datalog programs
溯源引导的 Datalog 程序合成
利用查询溯源信息引导 CEGIS，从输入输出规约高效合成 Datalog 程序。
POPL 4(POPL)2019匹配度 3/10引用 47程序合成逻辑与约束编程
P2 Detecting critical bugs in SMT solvers using blackbox mutational fuzzing
基于黑盒变异模糊测试的 SMT 求解器关键缺陷检测
提出 STORM，一种黑盒变异模糊测试技术，用于发现 SMT 求解器中的关键缺陷。
FSE Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2020匹配度 3/10引用 46测试、调试与修复逻辑与约束编程
P2 Scallop: A Language for Neurosymbolic Programming
Scallop：一种神经符号编程语言
提出 Scallop 语言，用基于 Datalog 的可微逻辑编程统一深度学习与符号推理。
PLDI 7(PLDI)2023匹配度 3/10引用 38机器学习与程序语言逻辑与约束编程
P2 Parameterized model counting for string and numeric constraints
字符串与数值约束的参数化模型计数
提出面向字符串与数值约束的参数化模型计数求解器，用多轨 DFA 计数解，支持任意大界与混合约束。
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 3/10引用 33逻辑与约束编程程序分析与抽象解释
P2 Maximal multi-layer specification synthesis
最大化多层规约合成
MARS 将输入输出样例、文本描述和部分代码构成的多层规约归约为 Max-SMT，并用 LSTM 与关联规则学习用户意图。
FSE Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2019匹配度 3/10引用 31程序合成机器学习与程序语言逻辑与约束编程
P2 Semantics-guided synthesis
语义引导的程序合成
提出 SemGuS 框架，允许以递归大步步语义定义合成问题，并用 CHC 证明搜索同时合成程序与证明不可实现性。
POPL 5(POPL)2021匹配度 3/10引用 31程序合成形式语义逻辑与约束编程
P2 Fuzzing Symbolic Expressions
模糊测试符号表达式
提出近似求解器 FUZZY-SAT，用模糊测试技术判定符号公式可满足性，作为混合模糊测试中 SMT 求解的替代与补充。
ICSE 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)2021匹配度 3/10引用 30测试、调试与修复逻辑与约束编程
P2 Automatically testing string solvers
自动测试字符串求解器
针对字符串 SMT 求解器难以可靠检测不健全性的问题，提出自动测试方法以暴露其错误答案。
ICSE Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering2020匹配度 3/10引用 28测试、调试与修复逻辑与约束编程
P2 Fuzzing SMT solvers via two-dimensional input space exploration
通过二维输入空间探索对 SMT 求解器进行模糊测试
提出 Falcon，同时探索公式空间与配置空间，利用二者关联和自适应变异高效发现 SMT 求解器深层缺陷。
ISSTA Proceedings of the 30th ACM SIGSOFT International Symposium on Software Testing and Analysis2021匹配度 3/10引用 19测试、调试与修复逻辑与约束编程
P2 Skeletal approximation enumeration for SMT solver testing
面向 SMT 求解器测试的骨架近似枚举
提出轻量、通用的骨架近似枚举（SAE）技术，用于测试所有一阶理论的 SMT 求解器并发现大量真实缺陷。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 3/10引用 19测试、调试与修复逻辑与约束编程
P2 Goal-conflict likelihood assessment based on model counting
基于模型计数的目标冲突可能性评估
提出以模型计数量化目标冲突发生可能性，服务于目标导向需求工程的风险评估。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 3/10引用 19逻辑与约束编程领域特定语言与建模
P2 Solving String Constraints with Lengths by Stabilization
通过稳定化求解带长度的字符串约束
提出基于稳定化的字符串约束求解算法，可处理长度约束与不等关系，并集成到 SMT 求解器。
OOPSLA 7(OOPSLA2)2023匹配度 3/10引用 17逻辑与约束编程逻辑与自动机
P2 Debugging Large-scale Datalog
调试大规模 Datalog
提出可扩展的自底向上 Datalog 溯源调试策略与定点语义，并集成到 Soufflé 高效实现。
TOPLAS 42(2)2020匹配度 3/10引用 17逻辑与约束编程测试、调试与修复
P2 On Interpolation and Symbol Elimination in Theory Extensions
论理论扩展中的插值与符号消去
研究理论扩展中插值与符号消去的层次化方法，并推广至基理论仅有可量词消去模型完备的情形。
LMCS vol.Volume 14, Issue 32018匹配度 3/10引用 17逻辑与自动机逻辑与约束编程
P2 A symbolic model checking approach to the analysis of string and length constraints
面向字符串与长度约束分析的符号模型检测方法
提出用长度编码自动机与符号模型检测求解字符串和长度约束，可处理现有方法难解的问题。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 3/10引用 16逻辑与约束编程程序验证
P2 Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs
基于模板的多项式程序合成的代数几何算法
提出用代数几何定理将基于模板的多项式程序合成直接归约为二次规划，避免量词消去并保持半完备性。
OOPSLA 7(OOPSLA1)2023匹配度 3/10引用 15程序合成逻辑与约束编程
P2 Seminaïve evaluation for a higher-order functional language
面向高阶函数式语言的半朴素求值
将 Datalog 的半朴素求值扩展到 Datafun 的高阶函数式语言，支持一等关系与高阶函数递归。
POPL 4(POPL)2019匹配度 3/10引用 15逻辑与约束编程函数式编程
P2 Constraint-Based Refactoring
基于约束的重构
将基于约束的重构从类型推广到名称、位置、可访问性等属性，并给出工具正确性条件与实现算法。
TOPLAS 40(1)2018匹配度 3/10引用 15编程环境与开发者工具逻辑与约束编程
P2 Improving Bit-Blasting for Nonlinear Integer Constraints
改进非线性整数约束的 Bit-Blasting
针对困难非线性乘法、搜索空间与冗余问题改进位爆破，实现 BLAN 并在 SMT(QF_NIA) 上超越现有求解器。
ISSTA Proceedings of the 32nd ACM SIGSOFT International Symposium on Software Testing and Analysis2023匹配度 3/10引用 14逻辑与约束编程
P2 Declarative smart contracts
声明式智能合约
提出声明式语言 DeCon，用关系约束建模智能合约并规格化合约级属性，可编译为带运行时监控的 Solidity。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 3/10引用 14领域特定语言与建模逻辑与约束编程
P2 Satisfiability modulo fuzzing: a synergistic combination of SMT solving and fuzzing
Satisfiability modulo fuzzing：SMT 求解与模糊测试的协同组合
提出 Sādhak，将模糊测试与 SMT 求解协同用于含闭盒函数的约束求解。
OOPSLA 6(OOPSLA2)2022匹配度 3/10引用 13逻辑与约束编程测试、调试与修复
P2 Validating SMT Solvers via Skeleton Enumeration Empowered by Historical Bug-Triggering Inputs
利用历史缺陷触发输入进行骨架枚举以验证 SMT 求解器
提出 HistFuzz，从历史缺陷触发公式提取骨架并用关联规则枚举原子公式，以模糊测试 SMT 求解器并发现大量新缺陷。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 3/10引用 12测试、调试与修复逻辑与约束编程
P2 Resource-Guided Configuration Space Reduction for Deep Learning Models
资源引导的深度学习模型配置空间缩减
提出 DnnSAT，用代价模型与 SMT 求解在 AutoML 前缩减不满足资源约束的配置空间，加速 HPO 与 NAS。
ICSE 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)2021匹配度 3/10引用 12逻辑与约束编程机器学习与程序语言
P2 VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints
VeriEQL：带完整性约束的复杂 SQL 查询的有界等价性验证
提出首个基于 SMT 的复杂 SQL 查询有界等价性验证方法，可证明与反驳查询等价性并生成反例。
OOPSLA 8(OOPSLA1)2024匹配度 3/10引用 12程序验证逻辑与约束编程
P2 TensileFuzz: facilitating seed input generation in fuzzing via string constraint solving
TensileFuzz：通过字符串约束求解促进模糊测试中的种子输入生成
提出用字符串约束求解生成可增长的种子输入，并结合回归与梯度下降，显著提升路径覆盖。
ISSTA Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis2022匹配度 3/10引用 11测试、调试与修复逻辑与约束编程
P2 On the Expressive Power of String Constraints
论字符串约束的表达能力
系统比较20种字符串约束逻辑理论的语言表达能力，并研究跨理论可表达性的可判定性。
POPL 7(POPL)2023匹配度 3/10引用 11逻辑与自动机逻辑与约束编程
P2 Bring Your Own Data Structures to Datalog
把自定义数据结构带入 Datalog
提出 Byods：一种嵌入 Rust 的 DSL，使 Datalog 规则对关系的数据结构表示参数化，从而突破引擎内置表示带来的算法复杂度瓶颈。
OOPSLA 7(OOPSLA2)2023匹配度 3/10引用 11逻辑与约束编程领域特定语言与建模
P2 Consistency-preserving propagation for SMT solving of concurrent program verification
面向并发程序验证的 SMT 求解中的一致性保持传播
提出一致性保持的预防式传播方法，使并发程序验证的 SMT 序理论求解可省略一致性检查与冲突子句生成。
OOPSLA 6(OOPSLA2)2022匹配度 3/10引用 11程序验证逻辑与约束编程
P2 Grisette: Symbolic Compilation as a Functional Programming Library
Grisette：将符号编译作为函数式编程库
提出纯函数式、静态类型的符号求值库 Grisette，以有序守卫合并路径，显著缩小约束并加速求解。
POPL 7(POPL)2023匹配度 3/10引用 10函数式编程逻辑与约束编程领域特定语言与建模
P2 TestMC
TestMC：模型计数器的差分与蜕变测试
提出 TestMC 框架，用差分/蜕变测试与有界穷举输入生成测试模型计数器，发现三个工具缺陷。
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 3/10引用 9测试、调试与修复逻辑与约束编程
P2 Reasoning with Finite Sets and Cardinality Constraints in SMT
SMT 中带基数约束的有限集合推理
提出一种结合成员约束与基数约束的有限集合判定演算，并用图增量跟踪重叠区域。
LMCS vol.Volume 14, Issue 42018匹配度 3/10引用 9逻辑与约束编程
P2 Datalog-based scalable semantic diffing of concurrent programs
基于 Datalog 的并发程序可扩展语义差分
提出基于 Datalog 的快速近似静态分析，通过识别差异化数据流边来计算并发程序的同步语义差异。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 3/10引用 8程序分析与抽象解释逻辑与约束编程并发、并行与内存模型
P2 Optimal CHC Solving via Termination Proofs
基于终止性证明的最优 CHC 求解
提出将最优 CHC 求解的最优性检查归约到终止性分析，并用约束合成终止论证来实现。
POPL 7(POPL)2023匹配度 3/10引用 8逻辑与约束编程程序验证
P2 Accelerating all-SAT computation with short blocking clauses
利用短阻塞子句加速 all-SAT 计算
提出基于 backbone 的 all-SAT 求解器 BASolver，通过缩短阻塞子句加速全可满足赋值枚举。
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 3/10引用 6逻辑与约束编程
P2 SMT2Test: From SMT Formulas to Effective Test Cases
SMT2Test：从 SMT 公式到有效测试用例
提出将 SMT 公式转换为程序、以可满足性作为测试预言来测试程序验证器的方法与框架。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 6测试、调试与修复逻辑与约束编程
P2 A Typed Multi-level Datalog IR and Its Compiler Framework
带类型的多级 Datalog 中间表示及其编译器框架
提出首个通用 Datalog 编译器框架，以可扩展的带类型多级 IR 支持任意前端、逐层优化与多种后端。
OOPSLA 8(OOPSLA2)2024匹配度 3/10引用 6逻辑与约束编程编译与代码生成
P2 It's Not a Feature, It's a Bug: Fault-Tolerant Model Mining from Noisy Data
这不是特性，而是 Bug：从噪声数据中进行容错模型挖掘
提出用 Partial Max-SAT 从含噪执行轨迹中挖掘确定自动机，允许忽略最少故障观测且无需预处理。
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 3/10引用 5逻辑与自动机逻辑与约束编程
P2 Fixing Privilege Escalations in Cloud Access Control with MaxSAT and Graph Neural Networks
用 MaxSAT 和图神经网络修复云访问控制中的权限提升
提出 IAMPERE，用 GNN 剪枝与 MaxSAT 为 IAM 权限提升错误生成近似最小修复补丁。
ASE 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)2023匹配度 3/10引用 5安全与隐私逻辑与约束编程机器学习与程序语言
P2 Finding and Understanding Incompleteness Bugs in SMT Solvers
发现并理解 SMT 求解器中的不完备性缺陷
提出 Janus，用保持可满足性的变异测试 SMT 求解器，发现并理解返回 unknown 的不完备性缺陷。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 3/10引用 5测试、调试与修复逻辑与约束编程
P2 Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
基于半定规划的多项式程序不变式合成
用半定规划松弛与鲁棒优化合成多项式程序不变式，分别求解强、弱不变式合成问题并给出理论保证。
TOPLAS 47(1)2025匹配度 3/10引用 5程序验证逻辑与约束编程
P2 CSS Minification via Constraint Solving
基于约束求解的 CSS 最小化
将 CSS 规则合并最小化归约为 CSS 图优化，并用 SMT/Max-SAT 求解，实现语义保持的压缩。
TOPLAS 41(2)2019匹配度 3/10引用 5逻辑与约束编程编译与代码生成
P2 Diagnosis via Proofs of Unsatisfiability for First-Order Logic with Relational Objects
基于不可满足性证明的带关系对象一阶逻辑诊断
为 FOL* 不可满足性结果定义证明格式与规则，并给出证明校验与基于证明的诊断方法，用以解释不可满足的成因。
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 3/10引用 4逻辑与约束编程定理证明与证明工程
P2 State Merging with Quantifiers in Symbolic Execution
符号执行中带量词的状态合并
提出基于量词的状态合并方法，通过动态分组和专用求解过程减少约束编码爆炸。
FSE Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2023匹配度 3/10引用 4程序分析与抽象解释逻辑与约束编程
P2 Modularity and Combination of Associative Commutative Congruence Closure Algorithms enriched with Semantic Properties
融入语义性质的结合交换同余闭包算法的模块化与组合
提出模块化 AC 同余闭包算法，可组合幂等、可消去、群等语义性质，便于集成到 SMT 求解器。
LMCS vol.Volume 19, Issue 12023匹配度 3/10引用 4逻辑与约束编程定理证明与证明工程
P2 From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems
从 SMT 到 ASP：求解 Datalog 综合中“规则选择”问题的基于求解器的方法
提出三种基于求解器的方法求解 Datalog 规则选择综合问题，其中编码为 ASP 的方案比现有技术快约 9 倍且综合出更高质量的程序。
POPL 7(POPL)2023匹配度 3/10引用 4程序合成逻辑与约束编程
P2 Synthesizing MILP Constraints for Efficient and Robust Optimization
为高效且鲁棒的优化合成 MILP 约束
提出基于 SyGuS 的方法，从布尔逻辑规约自动合成高质量 MILP 线性约束。
PLDI 7(PLDI)2023匹配度 3/10引用 4程序合成逻辑与约束编程
P2 Uniform Interpolants in EUF: Algorithms using DAG-representations
EUF 中的一致插值：使用 DAG 表示的算法
提出两种基于项 DAG 表示的算法，用于在 EUF 中计算无量词一致插值，并给出正确性与完备性证明。
LMCS vol.Volume 18, Issue 22022匹配度 3/10引用 4逻辑与自动机逻辑与约束编程
P2 Deep Combination of CDCL(T) and Local Search for Satisfiability Modulo Non-Linear Integer Arithmetic Theory
CDCL(T) 与局部搜索的深度结合：求解非线性整数算术理论的 SMT 问题
提出两层混合框架 HybridSMT，深度融合 CDCL(T) 与随机局部搜索求解 SMT(NIA)，显著提升求解性能。
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 3/10引用 3逻辑与约束编程
P2 Constrained LTL Specification Learning from Examples
从示例中学习带约束的 LTL 规约
提出带约束的 LTL 学习问题，用一阶关系逻辑编码并归约到 MaxSAT，实现 ATLAS 工具。
ICSE 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)2025匹配度 3/10引用 3逻辑与自动机逻辑与约束编程
P2 Quantitative relational modelling with QAlloy
QAlloy 的定量关系建模
将整数内化到关系，扩展 Alloy 以优雅支持定量需求，并提供基于 SMT 的无界分析引擎。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 3/10引用 3领域特定语言与建模逻辑与约束编程
P2 Data-Driven Design and Evaluation of SMT Meta-Solving Strategies: Balancing Performance, Accuracy, and Cost
数据驱动的 SMT 元求解策略设计与评估：平衡性能、准确性与成本
提出并评估四类 SMT 元求解策略，以在性能、准确性与成本间取得平衡。
ASE 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)2021匹配度 3/10引用 3逻辑与约束编程
P2 A Resolution-Based Interactive Proof System for UNSAT
面向 UNSAT 的基于归结的交互式证明系统
将竞争性交互证明归约为算术化问题，并给出首个与 Davis-Putnam 归结竞争的 UNSAT 交互协议。
LMCS vol.Volume 22, Issue 22026匹配度 3/10引用 3逻辑与约束编程逻辑与自动机
P2 Inductive Approach to Spacer
Spacer 的归纳方法
用结构归纳重构 Spacer，统一 Spacer 与 GPDR，并分析其反驳完备性问题。
PLDI 8(PLDI)2024匹配度 3/10引用 3程序验证逻辑与约束编程
P2 Generating efficient solvers from constraint models
从约束模型生成高效求解器
提出模型驱动方法 SoGen，用 DSL PDL 建模组合问题，自动分析问题性质并合成高效专用求解器（C 程序）。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 3/10引用 2领域特定语言与建模逻辑与约束编程
P2 FMplex: Exploring a Bridge between Fourier-Motzkin and Simplex
FMplex：探索 Fourier-Motzkin 与单纯形法之间的桥梁
提出 FMplex，用量词消去处理线性实数算术合取，通过分支将最坏复杂度从双指数降至单指数。
LMCS vol.Volume 21, Issue 22025匹配度 3/10引用 2逻辑与约束编程
P2 Validating SMT Rewriters via Rewrite Space Exploration Supported by Generative Equality Saturation
通过生成式等式饱和支持的改写空间探索验证 SMT 重写器
提出 Aries，用拟态变异与生成式等式饱和探索 SMT 重写空间，验证重写系统并发现真实缺陷。
OOPSLA 9(OOPSLA2)2025匹配度 3/10引用 2测试、调试与修复逻辑与约束编程
P2 Interactive Bitvector Reasoning using Verified Bit-Blasting
基于已验证位爆破的交互式位向量推理
提出首个端到端已验证的位爆破器 bv_decide，将高效位向量推理作为 Lean 交互式证明 tactic，并支持反例生成。
OOPSLA 9(OOPSLA2)2025匹配度 3/10引用 2定理证明与证明工程逻辑与约束编程
P2 Parse this! Summoning Context-Sensitive Inputs with Goblin
解析这个！用 Goblin 召唤上下文敏感输入
提出 Goblin，基于带语义约束的上下文无关文法，借助 SMT 求解器生成满足上下文敏感约束的测试输入。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 3/10引用 1测试、调试与修复逻辑与约束编程
P2 DALEQ - Explainable Equivalence for Java Bytecode
DALEQ：Java 字节码的可解释等价性
提出 DALEQ，将 Java 字节码反汇编为关系数据库并用 Datalog 规则归一化，可解释地判定重建二进制等价性。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10引用 1程序分析与抽象解释逻辑与约束编程
P2 NRAgo: Solving SMT(NRA) Formulas with Gradient-Based Optimization
NRAgo：使用基于梯度的优化求解 SMT(NRA) 公式
提出混合 SMT(NRA) 求解器 NRAgo，将梯度优化与代数求解结合，大幅加速可满足实例。
ASE 2023 38th IEEE/ACM International Conference on Automated Software Engineering (ASE)2023匹配度 3/10引用 1逻辑与约束编程
P2 Effectively Analyzing Evolving Software with Differential Facts
使用差分事实有效分析演化软件
提出统一表示与 DIFFBASE 工具，用差分事实存储并查询软件演化历史中的关系与变更知识。
ASE 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE)2021匹配度 3/10引用 1程序分析与抽象解释逻辑与约束编程
P2 Dynamic algorithm selection for SMT
SMT 的动态算法选择
提出基于最近邻分类与运行时估计的在线 SMT 求解器选择方法，实现 MedleySolver，选择近乎最优且求解快三倍。
ASE Proceedings of the 35th IEEE/ACM International Conference on Automated Software Engineering2020匹配度 3/10引用 1逻辑与约束编程机器学习与程序语言
P2 Theory and practice of string solvers (invited talk abstract)
字符串求解器的理论与实践（特邀报告摘要）
回顾 HAMPI——最早实用的字符串约束求解器之一——及其对字符串求解理论与应用的广泛影响。
ISSTA Proceedings of the 28th ACM SIGSOFT International Symposium on Software Testing and Analysis2019匹配度 3/10引用 1逻辑与约束编程
P2 Extended Resolution Clause Learning via Dual Implication Points
基于双蕴含点的扩展归结子句学习
提出基于双蕴含点的扩展归结子句学习算法，在CDCL SAT求解器中动态引入新变量，提升Tseitin与XOR类公式求解性能。
LMCS vol.Volume 22, Issue 22026匹配度 3/10引用 1逻辑与约束编程
P2 Checking δ-Satisfiability of Reals with Integrals
检查含积分的实数的 δ-可满足性
扩展 δ-决策过程以处理含积分的实数约束，并实现工具 ∫dReal 支持验证与合成。
OOPSLA 9(OOPSLA1)2025匹配度 3/10引用 1逻辑与约束编程程序验证
P2 The Power of Regular Constraint Propagation
正则约束传播的力量
提出并实现正则约束传播方法，可可靠且完备地求解一大类字符串约束，并显著提升 OSTRICH 求解器性能。
OOPSLA 9(OOPSLA2)2025匹配度 3/10引用 1逻辑与约束编程逻辑与自动机
P2 Bounded Quantifier Instantiation for Checking Inductive Invariants
用于检查归纳不变式的有界量词实例化
提出有界视界量词实例化，使 SMT 检查归纳不变式终止，并证明其至少等价于手工 instrumentation。
LMCS vol.Volume 15, Issue 32019匹配度 3/10引用 1程序验证逻辑与约束编程
P2 Subsumption Algorithms for Three-Valued Geometric Resolution
三值几何归结中的包含算法
将三值几何归结的包含/匹配归约为广义约束满足，提出直接算法、SAT 编码与局部一致性过滤。
LMCS vol.Volume 14, Issue 42018匹配度 3/10引用 1定理证明与证明工程逻辑与约束编程
P2 QSolver: A Quantum Constraint Solver
QSolver：一种量子约束求解器
提出首个量子约束求解器 QSolver，将量子程序与多时刻约束符号化并用 SMT 求解满足约束的量子态。
ICSE Proceedings of the IEEE/ACM 48th International Conference on Software Engineering2026匹配度 3/10量子与概率编程逻辑与约束编程程序验证
P2 Accelerating IC3 Verification by Exploiting Unsatisfiable Cores and Satisfying Models
利用不可满足核心与可满足模型加速 IC3 验证
提出复用不可满足核心与可满足模型的 IC3 验证加速方法，显著减少求解器调用并提速。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 3/10程序验证逻辑与约束编程
P2 Performance Improvement of Automated Test Input Data Generation by Using Value Concretization
使用值具体化提升自动化测试输入数据生成的性能
提出值具体化变换约束逻辑公式，缓解 COBOL 测试输入生成中字节级建模带来的求解器性能下降。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 3/10测试、调试与修复逻辑与约束编程
P2 FM4MC: Improving Feature Models for Microservice Chains—Towards More Efficient Configuration and Validation
FM4MC：改进微服务链的特征模型——面向更高效的配置与验证
提出 FM4MC，通过切片为部分特征模型并按复杂度选择性 SAT 求解，大幅加速微服务链特征模型验证。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 3/10领域特定语言与建模逻辑与约束编程
P2 Towards Output Directed Debugging of Finite Model Finders
走向有限模型查找器的输出导向调试
提出输出导向调试工作流：用户通过编辑模型查找器生成的场景而非形式约束来调试模型。
FSE Proceedings of the 34th ACM International Conference on the Foundations of Software Engineering2026匹配度 3/10逻辑与约束编程编程环境与开发者工具
P2 Automated Combinatorial Test Generation for Alloy
Alloy 规约的自动化组合测试生成
提出 COMBA：一种无需人工干预、基于组合覆盖准则的 Alloy 规约自动化测试生成技术。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10测试、调试与修复逻辑与约束编程
P2 First-Order Quantified Separator in Alloy Analyzer
Alloy Analyzer 中的一阶量化分离器
提出 Folloy，将一阶逻辑规约学习编码为 Alloy 中的约束满足问题，并用 Max-SAT 保证所学公式规模最小。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10程序合成逻辑与约束编程
P2 Efficient and Verifiable Proof Logging for MaxSAT Solving
面向 MaxSAT 求解的高效可验证证明日志
为 core-guided OLL MaxSAT 求解器提出首个原生证明日志框架，形式化推理规则并实现可自动检验的最优性证书。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10程序验证逻辑与约束编程
P2 Relia: Accelerating the Analysis of Cloud Access Control Policies
Relia：加速云访问控制策略分析
提出 Relia，用字符串等价类将正则约束重写为整数约束，加速云访问控制策略的 SMT 分析。
ASE 2025 40th IEEE/ACM International Conference on Automated Software Engineering (ASE)2025匹配度 3/10安全与隐私逻辑与约束编程
P2 Synthesis of Sound and Precise Storage Cost Bounds via Unsound Resource Analysis and Max-SMT
通过不健全资源分析与 Max-SMT 合成健全且精确的存储成本界
先用不健全静态资源分析获得精确存储成本界，再用 Max-SMT 修正以恢复健全性，用于以太坊 gas 分析。
ISSTA Proceedings of the 33rd ACM SIGSOFT International Symposium on Software Testing and Analysis2024匹配度 3/10程序分析与抽象解释逻辑与约束编程
P2 MCBAT: a practical tool for model counting constraints on bounded integer arrays
MCBAT：一个有界整数数组约束模型计数的实用工具
提出 MCBAT 工具，将有界整数数组约束归约到 LIA，并用 Barvinok 算法进行模型计数。
FSE Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2020匹配度 3/10逻辑与约束编程程序分析与抽象解释
P2 A Fixed Point Theorem on Lexicographic Lattice Structures
词典序格结构上的一个不动点定理
提出词典序格结构上的不动点定理，统一非单调形式体系的最小不动点语义。
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 3/10形式语义逻辑与约束编程
P2 Sound and Complete Invariant-Based Heap Encodings
可靠且完备的基于不变式的堆编码
提出时间索引堆不变式，借助未解释谓词与预言变量将堆程序验证归约为整数程序验证，并首次同时实现可靠性与完备性。
OOPSLA 10(OOPSLA1)2026匹配度 3/10程序验证逻辑与约束编程
P2 &inator: Correct, Precise C-to-Rust Interface Translation
&inator：正确、精确的 C 到 Rust 接口翻译
提出首个基于约束求解的正确且精确的 C 到 Rust 接口翻译方法，生成满足借用检查的最简 Rust 声明。
PLDI 10(PLDI)2026匹配度 3/10编译与代码生成逻辑与约束编程
P2 Universal Scalability in Declarative Program Analysis (with Choice-Based Combination Pruning)
声明式程序分析中的通用可扩展性（基于 Choice 的组合剪枝）
利用 Datalog 的 choice 构造自适应剪枝关系投影，使既有声明式程序分析框架在几乎不损失完备性下大幅加速。
OOPSLA 9(OOPSLA2)2025匹配度 3/10逻辑与约束编程程序分析与抽象解释
P2 Decision procedures for path feasibility of string-manipulating programs with complex operations
复杂操作字符串操作程序的路径可行性判定过程
提出保证字符串操作程序路径可行性可判定的语义条件，并实现可扩展求解器 OSTRICH。
POPL 3(POPL)2019匹配度 2/10引用 80逻辑与自动机逻辑与约束编程
P2 Multi-objective integer programming approaches for solving optimal feature selection problem
求解最优特征选择问题的多目标整数规划方法
揭示软件产品线最优特征选择的多目标二值整数线性规划本质，并提出可线性时间生成完整Pareto前沿的高效方法。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 2/10引用 45领域特定语言与建模逻辑与约束编程
P2 Quadratic Word Equations with Length Constraints, Counter Systems, and Presburger Arithmetic with Divisibility
带长度约束的二次词方程、计数器系统与带整除的 Presburger 算术
通过计数器系统与带整除 Presburger 算术，给出 flat 二次词方程长度约束的可判定性与复杂度上界。
LMCS vol.Volume 17, Issue 42021匹配度 2/10引用 40逻辑与自动机逻辑与约束编程
P2 Baital: an adaptive weighted sampling approach for improved t-wise coverage
Baital：一种提升 t-wise 覆盖率的自适应加权采样方法
提出 Baital，利用基于文字加权函数的自适应加权采样生成高 t-wise 覆盖率的测试集，显著优于均匀采样。
FSE Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2020匹配度 2/10引用 38测试、调试与修复逻辑与约束编程
P2 A unified approach to solving seven programming problems (functional pearl)
一种解决七个编程问题的统一方法（函数式珍珠）
提出用 miniKanren 约束逻辑编程统一解决 Racket 中七个编程挑战的优雅方法。
ICFP 1(ICFP)2017匹配度 2/10引用 35逻辑与约束编程函数式编程
P2 Combinatorial Register Allocation and Instruction Scheduling
组合寄存器分配与指令调度
提出基于约束编程的组合优化方法，统一求解寄存器分配与指令调度，生成优于 LLVM 的可执行代码。
TOPLAS 41(3)2019匹配度 2/10引用 34编译与代码生成逻辑与约束编程
P2 Active Inductive Logic Programming for Code Search
面向代码搜索的主动归纳逻辑编程
提出交互式代码搜索技术 ALICE，用主动归纳逻辑编程从用户正负反馈中推断并精化逻辑查询。
ICSE 2019 IEEE/ACM 41st International Conference on Software Engineering (ICSE)2019匹配度 2/10引用 33逻辑与约束编程编程环境与开发者工具
P2 The electrum analyzer: model checking relational first-order temporal specifications
Electrum 分析器：关系一阶时序规约的模型检测
提出 Electrum Analyzer，为 Alloy 关系逻辑扩展 LTL，并支持有界 SAT 与无界 SMV 模型检测及可视化加速。
ASE Proceedings of the 33rd ACM/IEEE International Conference on Automated Software Engineering2018匹配度 2/10引用 31程序验证逻辑与约束编程
P2 Local consistency as a reduction between constraint satisfaction problems
局部一致性作为约束满足问题之间的归约
提出一致性归约框架，用局部一致性刻画 promise CSP 的归约与硬度，并联系多态性与 Sherali-Adams 层级。
LICS Proceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science2024匹配度 2/10引用 29逻辑与约束编程逻辑与自动机
P2 Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses
Tseitin 还是不 Tseitin？CNF 变换对特征模型分析的影响
系统比较三种 CNF 变换对特征模型分析的正确性与性能影响，揭示 Tseitin 等变换并非总是适用。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 2/10引用 27逻辑与约束编程领域特定语言与建模
P2 Bounded Exhaustive Search of Alloy Specification Repairs
Alloy 规约修复的有界穷举搜索
提出 BeAFix，对有缺陷的 Alloy 规约进行有界穷举且可扩展的自动修复，并用断言剪枝。
ICSE 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)2021匹配度 2/10引用 26测试、调试与修复逻辑与约束编程
P2 Quantifying permissiveness of access control policies
量化访问控制策略的宽松程度
提出定量差分策略分析框架，用模型计数约束求解器量化访问控制策略的相对宽松程度。
ICSE Proceedings of the 44th International Conference on Software Engineering2022匹配度 2/10引用 25安全与隐私逻辑与约束编程
P2 Program Repair Guided by Datalog-Defined Static Analysis
由 Datalog 定义的静态分析引导的程序修复
提出 Datalog 符号执行技术，将程序修复归约为修改 Datalog 事实，实现通用静态程序修复框架。
FSE Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2023匹配度 2/10引用 23测试、调试与修复逻辑与约束编程
P2 Data-Oriented Differential Testing of Object-Relational Mapping Systems
面向数据的对象关系映射系统差分测试
首个系统化测试ORM系统的方法，结合差分测试与求解器生成数据，发现28个真实缺陷。
ICSE 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)2021匹配度 2/10引用 21测试、调试与修复逻辑与约束编程
P2 Simplified Algorithmic Metatheorems Beyond MSO: Treewidth and Neighborhood Diversity
超越 MSO 的简化算法元定理：树宽与邻域多样性
研究 MSO 扩展在树宽与邻域多样性图上的模型检测复杂度，给出 FPT/XP 算法与 CSP 归约方法。
LMCS vol.Volume 15, Issue 42019匹配度 2/10引用 21逻辑与自动机逻辑与约束编程
P2 Sparse Hashing for Scalable Approximate Model Counting
面向可扩展近似模型计数的稀疏哈希
设计稀疏哈希函数，以更小概率选变量生成短 XOR 约束，提升近似 #SAT 模型计数的可扩展性。
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10引用 20逻辑与约束编程
P2 Translation of Algorithmic Descriptions of Discrete Functions to SAT with Applications to Cryptanalysis Problems
将离散函数的算法描述翻译为 SAT 及其在密码分析问题中的应用
提出将离散函数算法描述归约为 SAT 的技术与 Transalg 工具，用于代数密码分析并构造攻击。
LMCS vol.Volume 16, Issue 12020匹配度 2/10引用 20逻辑与约束编程安全与隐私
P2 Nemo
Nemo：多准则测试套件最小化框架
将多准则测试套件最小化建模为整数非线性规划并转换为线性规划，以高效求最优解。
ICSE Proceedings of the 40th International Conference on Software Engineering2018匹配度 2/10引用 18测试、调试与修复逻辑与约束编程
P2 AutoCCAG: An Automated Approach to Constrained Covering Array Generation
AutoCCAG：约束覆盖数组生成的自动化方法
提出 AutoCCAG，利用自动算法配置与选择生成更小的约束覆盖数组，并首次报告 5-way CCAG 结果。
ICSE 2021 IEEE/ACM 43rd International Conference on Software Engineering (ICSE)2021匹配度 2/10引用 17测试、调试与修复逻辑与约束编程
P2 smartPip: A Smart Approach to Resolving Python Dependency Conflict Issues
smartPip：一种解决 Python 依赖冲突问题的智能方法
实证揭示 Python 依赖冲突新特征，提出基于 SMT 求解与虚拟环境复用的 smartPip 工具。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 2/10引用 17逻辑与约束编程编程环境与开发者工具
P2 Analyzing and Debugging Normative Requirements via Satisfiability Checking
基于可满足性检查分析并调试规范性需求
提出 N-Check，用可满足性检查自动发现并诊断规范性非功能需求中的冲突、冗余、过强限制与不足等问题。
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 2/10引用 15逻辑与约束编程
P2 Flexible and Optimal Dependency Management via Max-SMT
基于 Max-SMT 的灵活且最优的依赖管理
提出 Pacsolve 框架与 Maxnpm，用 Max-SMT 将依赖求解建模为可定制约束与多目标优化问题，替代 NPM 的贪心算法。
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 2/10引用 15逻辑与约束编程
P2 AlloyMax: bringing maximum satisfaction to relational specifications
AlloyMax：为关系规范带来最大满足
提出 AlloyMax，将最大满足/优化目标引入 Alloy 关系规范，使 SAT 无法处理的最优解分析成为可能。
FSE Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2021匹配度 2/10引用 10逻辑与约束编程领域特定语言与建模
P2 SparseAuto: An Auto-scheduler for Sparse Tensor Computations using Recursive Loop Nest Restructuring
SparseAuto：使用递归循环嵌套重构的稀疏张量计算自动调度器
提出基于递归循环嵌套重构的稀疏张量计算自动调度器，可生成渐近更优的调度与代码。
OOPSLA 8(OOPSLA2)2024匹配度 2/10引用 10编译与代码生成逻辑与约束编程
P2 ProFL: a fault localization framework for Prolog
ProFL：面向 Prolog 的故障定位框架
将基于频谱与变异的故障定位技术适配到 Prolog，并实现为开源命令行工具 ProFL，输出可疑子句。
ISSTA Proceedings of the 29th ACM SIGSOFT International Symposium on Software Testing and Analysis2020匹配度 2/10引用 8测试、调试与修复逻辑与约束编程
P2 The Complexity of Combinations of Qualitative Constraint Satisfaction Problems
定性约束满足问题组合的复杂度
证明在一大类 ω-范畴理论中，Nelson-Oppen 组合条件对并集 CSP 的多项式时间可解性也是必要的（除非 P=NP）。
LMCS vol.Volume 16, Issue 12020匹配度 2/10引用 8逻辑与约束编程逻辑与自动机
P2 On Almost-Uniform Generation of SAT Solutions: The power of 3-wise independent hashing
SAT 解的几乎均匀生成：3-独立哈希的威力
提出基于3-独立哈希的SAT解几乎均匀生成算法，在562个基准上全部成功而JVV超时544个。
LICS Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science2022匹配度 2/10引用 7逻辑与约束编程
P2 Efficient Slicing of Feature Models via Projected d-DNNF Compilation
通过投影 d-DNNF 编译实现特征模型的高效切片
提出投影 d-DNNF 编译，将特征模型切片与知识编译合并为一步，显著降低运行时间。
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 2/10引用 6领域特定语言与建模逻辑与约束编程
P2 Quacky: Quantitative Access Control Permissiveness Analyzer✱
Quacky：定量访问控制宽松度分析器
将云访问控制策略翻译为 SMT 公式，借助模型计数求解器量化并比较策略的宽松程度。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 2/10引用 5安全与隐私逻辑与约束编程
P2 Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates
Mobius：合成带有递归与发明谓词的关系查询
提出 Mobius，从数据中全自动合成含递归与发明谓词的关系查询，并用数据溯源加速搜索。
OOPSLA 7(OOPSLA2)2023匹配度 2/10引用 5程序合成逻辑与约束编程
P2 Infinite Probabilistic Databases
无限概率数据库
提出用有限点过程为无限概率数据库建模，并证明关系代数、聚合与 Datalog 查询在不可数概率空间中的可测性。
LMCS vol.Volume 18, Issue 12022匹配度 2/10引用 5形式语义逻辑与约束编程
P2 Discovering, quantifying, and displaying attacks
发现、量化并展示攻击
提出基于 Quality Calculus 的保护分析，可发现攻击、按代价量化最廉价攻击并生成攻击树。
LMCS vol.Volume 12, Issue 42017匹配度 2/10引用 5安全与隐私逻辑与约束编程
P2 Constraint Based Program Repair for Persistent Memory Bugs
面向持久内存错误的基于约束的程序修复
提出基于约束的程序修复方法，可修复持久内存的持久性与崩溃一致性错误并发现新修复策略。
ICSE Proceedings of the IEEE/ACM 46th International Conference on Software Engineering2024匹配度 2/10引用 4测试、调试与修复逻辑与约束编程
P2 AlloyInEcore: embedding of first-order relational logic into meta-object facility for automated model reasoning
AlloyInEcore：将一阶关系逻辑嵌入元对象设施以实现自动化模型推理
将一阶关系逻辑嵌入 MOF/Ecore，用静态语义自动检测不一致并补全模型。
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 2/10引用 4领域特定语言与建模逻辑与约束编程
P2 Modus: a Datalog dialect for building container images
Modus：一种用于构建容器镜像的 Datalog 方言
提出 Modus——一种用于构建容器镜像的 Datalog 方言，以约束构建参数交互。
FSE Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering2022匹配度 2/10引用 3领域特定语言与建模逻辑与约束编程
P2 Object-Oriented Fixpoint Programming with Datalog
用 Datalog 进行面向对象定点编程
设计 OODL 语言，将对象、动态分派和受控可变性融入 Datalog 式定点语义，并编译到 Datalog。
OOPSLA 8(OOPSLA2)2024匹配度 2/10引用 3逻辑与约束编程语言设计与特性编译与代码生成
P2 Scalable Sampling of Highly-Configurable Systems: Generating Random Instances of the Linux Kernel
高度可配置系统的可扩展采样：生成 Linux 内核的随机实例
提出基于可扩展逻辑组的新采样器，首次可对 Linux 内核这类超大可配置系统高效生成随机有效配置。
ASE Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering2022匹配度 2/10引用 2逻辑与约束编程领域特定语言与建模
P2 Initial Limit Datalog: a New Extensible Class of Decidable Constrained Horn Clauses
初始极限 Datalog：一类新的可扩展可判定约束霍恩子句
提出初始极限 Datalog，将可判定极限 DatalogZ 推广到高阶并支持任意合适背景理论。
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 2/10引用 2逻辑与自动机逻辑与约束编程
P2 Finite-Choice Logic Programming
有限选择逻辑编程
提出有限选择逻辑编程，用选择代替否定表达多解，并实现 Dusa 求解器。
POPL 9(POPL)2025匹配度 2/10引用 2逻辑与约束编程形式语义
P2 Cutting the Cake: A Language for Fair Division
切蛋糕：一种公平分配语言
提出公平分配领域专用语言 Slice，将协议编译为逻辑约束并调用求解器自动验证无嫉妒性。
PLDI 7(PLDI)2023匹配度 2/10引用 2领域特定语言与建模逻辑与约束编程
P2 Automated Ambiguity Detection in Layout-Sensitive Grammars
布局敏感文法中的自动歧义检测
提出布局敏感文法的有界歧义检测方法，以SMT编码局部歧义并机器化验证，可找出最短歧义句。
OOPSLA 7(OOPSLA2)2023匹配度 2/10引用 2语言设计与特性逻辑与约束编程定理证明与证明工程
P2 torte: Reproducible Feature-Model Experiments à la Carte
torte：按需定制的可复现特征模型实验
提出开源工具 torte，集成现有工具与原创贡献，支持可复现、灵活的特征模型实验，并可分析 Linux 内核历史。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 2/10引用 1领域特定语言与建模逻辑与约束编程
P2 Can SAT Solvers Keep Up With the Linux Kernel's Feature Model?
SAT 求解器能跟上 Linux 内核的特征模型吗？
通过历史特征模型与历史 SAT 求解器的实证分析，发现 SAT 求解器整体跟不上 Linux 内核特征模型的增长。
ICSE Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering2026匹配度 2/10引用 1逻辑与约束编程领域特定语言与建模
P2 Explainable Port Mapping Inference with Sparse Performance Counters for AMD's Zen Architectures
面向 AMD Zen 架构的稀疏性能计数器可解释端口映射推断
修改 uops.info 的端口映射推断算法，使其仅依赖稀疏性能计数器，并用 SMT 驱动的反例引导方法推断 AMD Zen 的端口映射。
ASPLOS Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 32024匹配度 2/10引用 1语言与体系结构逻辑与约束编程
P2 Personalized Fuzzing: A Case Study with the FANDANGO Fuzzer on a GNSS Module (Short Paper)
个性化模糊测试：以 FANDANGO 模糊器在 GNSS 模块上的案例研究（短文）
展示约束引导的语法模糊器 FANDANGO 能生成100%合法且针对性强的输入，在 GNSS 模块上暴露潜在弱点。
ISSTA Proceedings of the 34th ACM SIGSOFT International Symposium on Software Testing and Analysis2025匹配度 2/10引用 1测试、调试与修复逻辑与约束编程
P2 DeployFix: Dynamic Repair of Software Deployment Failures via Constraint Solving
DeployFix：通过约束求解实现软件部署失败的动态修复
提出 DeployFix，用约束求解自动定位并修复动态部署环境中的配置冲突导致的部署失败。
ASE Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering2024匹配度 2/10引用 1逻辑与约束编程测试、调试与修复
P2 Constraint Satisfaction Problems over Finite Structures
有限结构上的约束满足问题
系统研究含关系与运算的有限结构上 CSP 的计算复杂度，给出代数条件并完成二元素结构分类
LICS 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)2021匹配度 2/10引用 1逻辑与约束编程逻辑与自动机
P2 AlloyMC: Alloy meets model counting
AlloyMC：Alloy 遇上模型计数
为 Alloy 扩展语法与后端以支持模型计数，让用户能统计给定公式的解的个数。
FSE Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2020匹配度 2/10引用 1逻辑与约束编程领域特定语言与建模
P2 Lazy product discovery in huge configuration spaces
巨大配置空间中的惰性产品发现
提出在巨大配置空间中惰性发现有效产品配置的方法，通过碎片化相互依赖的特征模型支持配置探索。
ICSE Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering2020匹配度 2/10引用 1领域特定语言与建模逻辑与约束编程
P2 Temporal Constraint Satisfaction Problems in Fixed-Point Logic
不动点逻辑中的时态约束满足问题
证明时态 CSP 在 Datalog 与（计数/秩）不动点逻辑中的可表达性，并给出完整分类，表明有限域 Maltsev 条件无法推广。
LICS Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science2020匹配度 2/10引用 1逻辑与自动机逻辑与约束编程
P2 Characterizing Sets of Theories That Can Be Disjointly Combined
刻画可不相交组合的理论集合
通过 Galois 连接刻画可与给定可判定理论集合不相交组合的最大理论类，并否证若干开放问题。
POPL 10(POPL)2026匹配度 2/10引用 1逻辑与约束编程逻辑与自动机
P2 Linear Programs with Conjunctive Database Queries
带合取数据库查询的线性规划
提出 LP(CQ) 语言，并用广义超树分解因子化答案集元素，以更少变量高效求解合取查询定义的线性规划。
LMCS vol.Volume 20, Issue 12024匹配度 2/10引用 1逻辑与约束编程领域特定语言与建模
P2 Saggitarius: A DSL for Specifying Grammatical Domains
Saggitarius：用于描述语法域的 DSL
提出 DSL Saggitarius 描述上下文无关文法族，并用半环解析与 MaxSAT 从示例数据推断最匹配文法。
OOPSLA 7(OOPSLA2)2023匹配度 2/10引用 1领域特定语言与建模逻辑与约束编程
P2 Prototyping a functional language using higher-order logic programming: a functional pearl on learning the ways of λProlog/Makam
使用高阶逻辑编程原型化函数式语言：一篇关于学习 λProlog/Makam 的函数式珍珠
展示如何用 λProlog/Makam 的高阶逻辑编程快速原型化带复杂类型系统的函数式语言实现。
ICFP 2(ICFP)2018匹配度 2/10引用 1逻辑与约束编程语言设计与特性