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 条
  • [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] ACL2s: "The ACL2 Sedan"
    Dillinger, Peter C.
    Manolios, Panagiotis
    Vroon, Daron
    Moore, J. Strother
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2007, 174 (02) : 3 - 18
  • [3] 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
  • [4] Proving with ACL2 the Correctness of Simplicial Sets in the Kenzo System
    Heras, Jonathan
    Pascual, Vico
    Rubio, Julio
    [J]. LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2011, 6564 : 37 - 51
  • [5] Executing in common lisp, proving in ACL2
    Andres, Mirian
    Lamban, Laureano
    Rubio, Julio
    [J]. TOWARDS MECHANIZED MATHEMATICAL ASSISTANTS, 2007, 4573 : 1 - +
  • [6] The Fundamental Theorem of Algebra in ACL2
    Gamboa, Ruben
    Cowles, John
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2018, (280): : 98 - 110
  • [7] Proving theorems about Java']Java and the JVM with ACL2
    Moore, JS
    [J]. MODELS, ALGEBRAS AND LOGIC OF ENGINEERING SOFTWARE, 2003, 191 : 227 - 290
  • [8] Formalizing rewriting in the ACL2 theorem prover
    Ruiz-Reina, JL
    Alonso, JA
    Hidalgo, MJ
    Martín-Mateos, FJ
    [J]. ARTIFICIAL INTELLIGENCE AND SYMBOLIC COMPUTATION, 2001, 1930 : 92 - 106
  • [9] Proceedings - 17th International Workshop on the ACL2 Theorem Prover and its Applications, ACL2 2022
    [J]. Electronic Proceedings in Theoretical Computer Science, EPTCS, 2022, 359
  • [10] ACL2
    Gamboa, R
    [J]. SEVENTEEN PROVERS OF THE WORLD, 2006, 3600 : 55 - 66
12345