ACL2s: "The ACL2 Sedan"

被引：19

作者：

Dillinger, Peter C. ^{[1
]}

Manolios, Panagiotis ^{[1
]}

Vroon, Daron ^{[1
]}

Moore, J. Strother ^{[2
]}

机构：

[1] Georgia Inst Technol, Coll Comp, Atlanta, GA 30332 USA

[2] Univ Texas Austin, Dept Comp Sci, Austin, TX 78712 USA

来源：

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE | 2007年 / 174卷 / 02期

基金：

美国国家科学基金会;

关键词：

ACL2; Eclipse; theorem proving; script management;

D O I：

10.1016/j.entcs.2006.09.018

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

ACL2 is the latest inception of the Boyer-Moore theorem prover, the 2005 recipient of the ACM Software System Award. In the hands of experts it feels like a finely tuned race car, and it has been used to prove some of the most complex theorems ever proved about commercially designed systems. Unfortunately, ACL2 has a steep learning curve. Thus, novices tend have a very different experience: they crash and burn. As part of a project to make ACL2 and formal reasoning safe for the masses, we have developed ACL2s, the ACL2 sedan. ACL2s includes many features for streamlining the learning process that are not found in ACL2. In general, the goal is to develop a tool that is "self-teaching," i.e., it should be possible for an undergraduate to sit down and play with it and learn how to program in ACL2 and how to reason about the programs she writes.

引用

页码：3 / 18

页数：16

共 50 条

[1] ACL2s: "The ACL2 sedan"
Dillinger, Peter C.
Manolios, Panagiotis
Vroon, Daron
Moore, J. Strother
[J]. 29TH INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING: ICSE 2007 COMPANION VOLUME, PROCEEDINGS, 2007, : 59 - +
[2] Data Definitions in the ACL2 Sedan
Chamarthi, Harsh Raju
Dillinger, Peter C.
Manolios, Panagiotis
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 27 - 48
[3] The ACL2 Sedan Theorem Proving System
Chamarthi, Harsh Raju
Dillinger, Peter
Manolios, Panagiotis
Vroon, Daron
[J]. TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2011, 6605 : 291 - 295
[4] Verification of GossipSub in ACL2s
Kumar, Ankit
von Hippel, Max
Manolios, Panagiotis
Nita-Rotaru, Cristina
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, 393 : 113 - 132
[5] ACL2s Systems Programming
Walter, Andrew T.
Manolios, Panagiotis
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2022, (359): : 134 - 150
[6] ACL2
Gamboa, R
[J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
[7] ACL2(ml): Machine-Learning for ACL2
Heras, Jonathan
Komendantskaya, Ekaterina
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 61 - 75
[8] Proving Skipping Refinement with ACL2s
Jain, Mitesh
Manolios, Panagiotis
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (192): : 111 - 127
[9] Iteration in ACL2
Kaufmann, Matt
Moore, J. Strother
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (327): : 16 - 31
[10] Automated Grading of Automata with ACL2s
Kumar, Ankit
Walter, Andrew
Manolios, Panagiotis
[J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, (375): : 77 - 91

← 1 2 3 4 5 →