第 10 届 ACL2 定理证明器及其应用国际研讨会论文集
计算机科学中的逻辑
2011-10-21 v1 数学软件
摘要
本卷收录了 2011 年 ACL2 国际研讨会(ACL2 Theorem Prover and its Applications)的论文集。该研讨会于 2011 年 11 月 3 日至 4 日在美国德克萨斯州奥斯汀举行。ACL2 2011 是 ACL2 定理证明器及其应用系列研讨会的第十届。本次研讨会与第十一届计算机辅助设计形式化方法会议(FMCAD'11)同期举办。ACL2 研讨会系列为研究人员提供了一个主要的技术论坛,用于展示和讨论对定理证明器的改进与扩展、ACL2 与其他系统的比较,以及 ACL2 在形式化验证或形式化数学中的应用。自 1999 年以来,研讨会大约每 18 个月举办一次。ACL2 是 Boyer-Moore 定理证明器家族的最新版本,Robert Boyer、Matt Kaufmann 和 J Strother Moore 因该系列工作获得了 2005 年 ACM 软件系统奖。ACL2 是最先进的自动推理系统,已成功应用于学术界、政府和工业界,用于计算系统的规范说明与验证。更多详情可在论文集及研讨会网页(www.cs.ru.nl/~julien/acl2-11/)中找到。
引用
@article{arxiv.1110.4473,
title = {Proceedings 10th International Workshop on the ACL2 Theorem Prover and its Applications},
author = {David Hardin and Julien Schmaltz},
journal= {arXiv preprint arXiv:1110.4473},
year = {2011}
}