what4:符号公式表示法和求解器交互库 源码

What4是一个用于表示符号术语并与可满足性和SMT求解器(例如Yices和Z3)进行通信的库。 它最初是项目的一部分,但是发现了与最初用途无关的用例,作为Crucible符号模拟器的表示语言,因此被拆分为一个单独的存储库。 有关What4及其使用方法的概述,请参阅软件包级别的 。 该材料基于国防高级研究计划局(DARPA)根据合同HR0011-19-C-0070提供的工作。 所表达的观点,观点和/或发现仅是作者的观点,不应被解释为代表美国国防部或美国政府的正式观点或政策。