The ACL2 Sedan Theorem Proving System

被引：0
|
作者：
Chamarthi, Harsh Raju [1 ]
Dillinger, Peter [1 ]
Manolios, Panagiotis [1 ]
Vroon, Daron [1 ]
机构：
[1] Northeastern Univ, Coll Comp & Informat Sci, Boston, MA 02115 USA
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS | 2011年 / 6605卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
The ACL2 Sedan theorem prover (ACL2s) is an Eclipse plug-in that provides a modern integrated development environment, supports several modes of interaction, provides a powerful termination analysis engine, and includes fully automatic bug-finding methods based on a synergistic combination of theorem proving and random testing. ACL2s is publicly available and open source. It has also been used in several sections of a required freshman course at Northeastern University to teach over 200 undergraduate students how to reason about programs.
引用
收藏
页码：291 / 295
页数：5
相关论文
共 50 条
  • [21] Polymorphic Types in ACL2
    Selfridge, Benjamin
    Smith, Eric
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (152): : 49 - 59
  • [22] An integration of HOL and ACL2
    Gordon, Michael J. C.
    Reynolds, James
    Hunt, Warren A., Jr.
    Kaufmann, Matt
    [J]. PROCEEDINGS OF FORMAL METHODS IN COMPUTER AIDED DESIGN, 2006, : 153 - +
  • [23] CHERI Concentrate in ACL2
    Kwan, Carl
    Xin, Yutong
    Young, William D.
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2023, (393):
  • [24] Nonstandard analysis in ACL2
    Gamboa, RA
    Kaufmann, M
    [J]. JOURNAL OF AUTOMATED REASONING, 2001, 27 (04) : 323 - 351
  • [25] Partial functions in ACL2
    Manolios, P
    Moore, JS
    [J]. JOURNAL OF AUTOMATED REASONING, 2003, 31 (02) : 107 - 127
  • [26] Perfect Numbers in ACL2
    Cowles, John
    Gamboa, Ruben
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2015, (192): : 53 - 59
  • [27] Android Platform Modeling and Android App Verification in the ACL2 Theorem Prover
    Smith, Eric
    Coglio, Alessandro
    [J]. VERIFIED SOFTWARE: THEORIES, TOOLS, AND EXPERIMENTS, 2016, 9593 : 183 - 201
  • [28] Partial Functions in ACL2
    Panagiotis Manolios
    J Strother Moore
    [J]. Journal of Automated Reasoning, 2003, 31 : 107 - 127
  • [29] Formalising Filesystems in the ACL2 Theorem Prover: an Application to FAT32
    Mehta, Mihir Parang
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (280): : 18 - 29
  • [30] Nonstandard Analysis in ACL2
    Ruben A. Gamboa
    Matt Kaufmann
    [J]. Journal of Automated Reasoning, 2001, 27 : 323 - 351
12345