Open Provable Foundation

2022年6月9日 (四) 07:39的版本

Open Provable Foundation（开放可证明基础）

Satisfiability Modulo Theories (SMT) 可满足性模理论指函数和关系符号在背景理论中进行解释的谓词逻辑公式的可满足性判定问题，SMT求解器已经成为软件工程、编程语言、信息安全领域的基础引擎。
SMT @ Microsoft SMT在微软很火
SMT-LIB
International Satisfiability Modulo Theories Competition (SMT-COMP) 国际可满足性模理论竞赛

Provably Awesome
ML 语言家族适用于形式语言、计算机辅助定理证明、证明助理、逻辑语言、一阶逻辑、论证软件、代码验证等形式化领域。
Haskell, Agda, Idris, Liquid Haskell 具有“证明即程序、命题为类型”的特征。
F*
ACL2
proof assistant
Coq
Isabelle
HOL = functional programming + logic HOL Interactive Theorem Prover 文档 HOL Theory Hierarchy (Theory Graph)
seL4 The world's most highly assured OS kernel, specification and proofs with isabelle. The seL4 Haskell Model Haskell
Trustworthy Systems Formal methods
Hardware description language for Formal verification

@@ 第14行： / 第14行： @@
 ==SMT==
-*[http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisfiability Modulo Theories (SMT)] [https://baike.sogou.com/v193442449.htm 可满足性模理论]指函数和关系符号在背景理论中进行解释的谓词逻辑公式的可满足性判定问题，SMT求解器已经成为软件工程、编程语言、信息安全领域的基础引擎。[https://leodemoura.github.io/files/mpi2009.pdf SMT @ Microsoft] SMT在微软很火
+*[http://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories Satisfiability Modulo Theories (SMT)] [https://baike.sogou.com/v193442449.htm 可满足性模理论]指函数和关系符号在背景理论中进行解释的谓词逻辑公式的可满足性判定问题，SMT求解器已经成为软件工程、编程语言、信息安全领域的基础引擎。
+*[https://leodemoura.github.io/files/mpi2009.pdf SMT @ Microsoft] SMT在微软很火
 *[https://smtlib.cs.uiowa.edu/ SMT-LIB]
 *[https://smt-comp.github.io/ International Satisfiability Modulo Theories Competition (SMT-COMP)] 国际可满足性模理论竞赛