ACL2

ACL2 is both a programming language in which you can model computer systems and a tool to help you prove properties of those models. ACL2 is part of the Boyer-Moore family of provers.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element

References in zbMATH (referenced in 246 articles , 1 standard article )

Showing results 1 to 20 of 246.
Sorted by year (citations)

1 2 3 ... 11 12 13 next

  1. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  2. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
  3. Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri: Iterated ultrapowers for the masses (2018)
  4. Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
  5. Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
  6. Friedl, Stefan: An elementary proof of the group law for elliptic curves (2017)
  7. Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan: Efficient, verified checking of propositional proofs (2017)
  8. Lambán, Laureano; Martín-Mateos, Francisco J.; Rubio, Julio; Ruiz-Reina, José-Luis: Using abstract stobjs in ACL2 to compute matrix normal forms (2017)
  9. Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
  10. Rashid, Adnan; Hasan, Osman: Formalization of transform methods using HOL Light (2017)
  11. Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
  12. Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
  13. Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
  14. Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in Coq (2016)
  15. Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
  16. Maletzky, Alexander: Mathematical theory exploration in Theorema: reduction rings (2016)
  17. Nipkow, Tobias: Automatic functional correctness proofs for functional search trees (2016)
  18. Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.: Reasoning about algebraic data types with abstractions (2016)
  19. Smith, Eric; Coglio, Alessandro: Android platform modeling and android app verification in the ACL2 theorem prover (2016) ioport
  20. Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)

1 2 3 ... 11 12 13 next