跳转到内容
Jason's Study

形式化方法 · 论文 · 第 1 组

待复核

返回论文全景索引

本分块共 35 条，稳定上限为 100 条。

论文Slug难度可信状态简介
ACL2 — 用纯 Lisp 当数学对象，机器证明工业级硬件正确acl2-2000unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Awodey-Warren — 把『相等的证明』看成两点之间的路径awodey-warren-2009unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Bounded Model Checking — 把硬件验证翻译成一道 SAT 题biere-bmc-1999unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Boogie — 写一次验证后端，多种证明语言复用boogie-2005unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CertiKOS — 把整个并发内核拆成 30 多层每层都被 Coq 证过certikos-2016unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Chapar — 第一个被机器证明的因果一致 KV 存储chapar-2016unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
NuSMV 2 — 把 BDD 和 SAT 两种验证引擎装进同一个开源工具cimatti-nusmv-2002unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CEGAR — 用反例自动改进抽象，让大软件能被验证clarke-cegar-2003unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Clarke-Emerson 1981 — 让机器自己检查并发程序对不对clarke-emerson-1981unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
CryptoVerif — 让计算机直接证密码协议在真实计算模型下安全cryptoverif-2008unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Cubical Type Theory — 让 Univalence 公理真的能算出结果cubical-type-theory-2018unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Dafny — 把”代码该满足的条件”直接写进语法，编译器自动证明dafny-2010unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Disel — 把分布式协议拆成可独立证明、可拼装的 Coq 模块disel-2018unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
EasyCrypt — 让密码学家的安全证明能被机器自动检查easycrypt-2011unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Frama-C — 一个开源平台把 C 程序的多种验证方法拼到一起frama-c-2012unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Graf-Saïdi — 用谓词把无限状态压成有限抽象graf-saidi-1997unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
HACL* — 用数学证明过的 C 加密代码，跑在你 Firefox 和 Linux 内核里hacl-star-2017unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
HOL Light — 不到 500 行 OCaml 写出能证开普勒猜想的证明助手hol-light-2009unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
SPIN — 让计算机帮你穷举并发程序的所有可能执行holzmann-spin-1997unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
HoTT Book — 把”相等”重定义为路径，再让数学和程序共用同一本教材hott-book-2013unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Hyperkernel — 让 SMT 求解器一键验证操作系统内核hyperkernel-2017unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Iris 2015 — 把并发推理拆成 monoid + invariant 两块积木iris-2015unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Isabelle/HOL — 让程序证明像写数学论文一样可读isabelle-hol-2002unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
McMillan SMV 1993 — 把状态空间从 10^6 推到 10^20 的符号模型检测mcmillan-smv-1993unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Nuprl — 第一个把 Martin-Löf 类型论搬上屏幕的证明助手nuprl-1986unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
ProVerif — 把密码协议翻成 Prolog 规则让计算机自己证安全proverif-2001unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
SLAM — 让 Windows 驱动 bug 自己撞到工具上slam-microsoftunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Tamarin — 让计算机自己证 Signal、TLS 1.3 这种带 DH 的协议是不是真安全tamarin-2012unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
VAMP — 把一颗有流水线、乱序、浮点和 cache 的处理器从门电路证到指令集vamp-verisoft-2006unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
VCC — 给并发 C 加注解，让 SMT 自动证它对vcc-2009unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Verdi — 在 Coq 里完整证明 Raft 协议的分布式系统验证框架verdi-2015unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Verisoft — 把整台计算机从门电路到邮件客户端全部用数学证完verisoft-2008unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Verus-SpecGym — 让机器检查规格是不是写对了verus-specgymunknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
VST — 把 C 程序的数学证明一路带到机器码vst-2014unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。
Why3 — 写一次程序规范，多个证明器一起来证why3-2013unknownUNVERIFIED暂无独立描述；可先从标题与正文定位开始。