第14届ACL2定理证明器及其应用国际研讨会论文集
计算机科学中的逻辑
2017-05-03 v1
摘要
本卷收录了第十四届ACL2定理证明器及其应用国际研讨会（ACL2 2017）的会议论文，该研讨会于2017年5月22-23日在美国德克萨斯州奥斯汀举行，为期两天。ACL2研讨会大约每18个月举办一次，为研究人员提供了一个技术论坛，以展示和讨论该定理证明器的改进与扩展、ACL2与其他系统的比较，以及ACL2在形式化验证中的应用。ACL2是一个最先进的自动化推理系统，已成功应用于学术界、政府和工业界，用于计算系统的规约与验证，以及计算机科学课程教学。Boyer、Kaufmann和Moore因其在ACL2及Boyer-Moore定理证明器家族其他证明器方面的工作荣获2005年ACM软件系统奖。ACL2 2017的会议录包括研讨会上发表的七篇技术论文和两篇扩展摘要。每篇投稿获得了两到三份评审。研讨会还包括三场邀请报告：Centaur Technology公司的Glenn Henry所作的“在具有基于仿真心态的组织中使用机械化数学”；Aesthetic Integration的Grant Passmore所作的“金融算法的形式化验证：进展与展望”；以及Oracle的Greg Grohoski所作的“使用ACL2验证Oracle的SPARC处理器”。研讨会还包括若干快报环节，讨论正在进行的研究及ACL2在工业界中的使用。
引用
@article{arxiv.1705.00766,
title = {Proceedings 14th International Workshop on the ACL2 Theorem Prover and its Applications},
author = {Anna Slobodova and Warren Hunt},
journal= {arXiv preprint arXiv:1705.00766},
year = {2017}
}