Pinaka：符号执行结合增量求解（竞赛贡献）
计算机科学中的逻辑
2020-02-21 v1
摘要
许多现代求解器提供增量 SAT 求解功能，可在多次调用间保留求解器状态。当需要将多个紧密相关的 SAT 查询输入求解器时，这是有益的。Pinaka 是一个符号执行引擎，它激进地利用增量 SAT 求解并结合急切的状态不可行性检查。它构建于 CProver/Symex 框架之上。Pinaka 支持广度优先搜索与深度优先搜索作为状态探索策略，以及部分与完全增量模式。对于 SVCOMP 2019，Pinaka 配置为使用部分增量模式与深度优先搜索策略。
引用
@article{arxiv.1903.02309,
title = {Pinaka: Symbolic Execution meets Incremental Solving (Competition Contribution)},
author = {Eti Chaudhary and Saurabh Joshi},
journal= {arXiv preprint arXiv:1903.02309},
year = {2020}
}
备注
5 Pages, 3 Figures, To be published under TOOLympics 2019 (TACAS 2019, part 3)