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 291 articles , 1 standard article )

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

1 2 3 ... 13 14 15 next

  1. Sumners, Rob (ed.); Chau, Cuong (ed.): Proceedings of the seventeenth international workshop on the ACL2 theorem prover and its applications, Austin, Texas, USA, May 26--27, 2022 (2022)
  2. Evangelidis, Alexandros; Parker, David: Quantitative verification of Kalman filters (2021)
  3. Guan, Yong; Zhang, Jingzhi; Wang, Guohui; Li, Ximeng; Shi, Zhiping; Li, Yongdong: Formalization of Euler-Lagrange equation set based on variational calculus in HOL light (2021)
  4. Hóu, Zhé; Sanan, David; Tiu, Alwen; Liu, Yang; Hoa, Koh Chuen; Dong, Jin Song: An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model (2021)
  5. Kaufmann, Matt; Moore, J Strother: Limited second-order functionality in a first-order setting (2020)
  6. Mehta, Mihir Parang; Cook, William R.: Separation logic-based verification atop a binary-compatible filesystem model (2020)
  7. Passmore, Grant (ed.); Gamboa, Ruben (ed.): Proceedings of the sixteenth international workshop on the ACL2 theorem prover and its applications worldwide, Planet Earth, May 28--29, 2020 (2020)
  8. Temel, Mertcan; Slobodova, Anna; Hunt, Warren A. jun.: Automated and scalable verification of integer multipliers (2020)
  9. Tsachouridis, Vassilios A.; Giantamidis, Georgios; Basagiannis, Stylianos; Kouramas, Kostas: Formal analysis of the Schulz matrix inversion algorithm: a paradigm towards computer aided verification of general matrix flow solvers (2020)
  10. Araújo, João; Kinyon, Michael; Robert, Yves: Varieties of regular semigroups with uniquely defined inversion (2019)
  11. Barthe, Gilles; Betarte, Gustavo; Campo, Juan Diego; Luna, Carlos: System-level non-interference of constant-time cryptography. I: Model (2019)
  12. Johansson, Moa: Lemma discovery for induction. A survey (2019)
  13. Li, Li-Ming; Shi, Zhi-Ping; Guan, Yong; Zhang, Qian-Ying; Li, Yong-Dong: Formalization of geometric algebra in HOL Light (2019)
  14. Moore, J Strother: Milestones from the Pure Lisp Theorem Prover to ACL2 (2019)
  15. Paulson, Lawrence C.; Nipkow, Tobias; Wenzel, Makarius: From LCF to Isabelle/HOL (2019)
  16. Raggi, Daniel; Stockdill, Aaron; Jamnik, Mateja; Garcia Garcia, Grecia; Sutherland, Holly E. A.; Cheng, Peter C.-H.: Inspection and selection of representations (2019)
  17. Wang, Meng; Tian, Cong; Zhang, Nan; Duan, Zhenhua; Du, Hongwei: Verifying a scheduling protocol of safety-critical systems (2019)
  18. Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
  19. Carette, Jacques; Farmer, William M.; Laskowski, Patrick: HOL Light QE (2018)
  20. Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)

1 2 3 ... 13 14 15 next