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
References in zbMATH (referenced in 252 articles , 1 standard article )
Showing results 1 to 20 of 252.
Sorted by year (citations)
- Alex A. Alemi, Francois Chollet, Niklas Een, Geoffrey Irving, Christian Szegedy, Josef Urban: DeepMath - Deep Sequence Models for Premise Selection (2018) arXiv
- Carette, Jacques; Farmer, William M.; Laskowski, Patrick: HOL Light QE (2018)
- Czajka, Łukasz; Kaliszyk, Cezary: Hammer for Coq: automation for dependent type theory (2018)
- Enayat, Ali; Kaufmann, Matt; McKenzie, Zachiri: Iterated ultrapowers for the masses (2018)
- Farmer, William M.: Incorporating quotation and evaluation into Church’s type theory (2018)
- Page, Rex; Gamboa, Ruben: Essential logic for computer science (2018)
- Cruz-Filipe, Luís; Heule, Marijn J. H.; Hunt Jr., Warren A.; Kaufmann, Matt; Schneider-Kamp, Peter: Efficient certified RAT verification (2017)
- Friedl, Stefan: An elementary proof of the group law for elliptic curves (2017)
- Heule, Marijn; Hunt, Warren jun.; Kaufmann, Matt; Wetzler, Nathan: Efficient, verified checking of propositional proofs (2017)
- 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)
- Nagele, Julian; Felgenhauer, Bertram; Zankl, Harald: Certifying confluence proofs via relative termination and rule labeling (2017)
- Rashid, Adnan; Hasan, Osman: Formalization of transform methods using HOL Light (2017)
- Aransay, Jesús; Divasón, Jose: Formalisation of the computation of the echelon form of a matrix in Isabelle/HOL (2016)
- Avigad, Jeremy; Lewis, Robert Y.; Roux, Cody: A heuristic prover for real inequalities (2016)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Formalization of real analysis: a survey of proof assistants and libraries (2016)
- Cano, Guillaume; Cohen, Cyril; Dénès, Maxime; Mörtberg, Anders; Siles, Vincent: Formalized linear algebra over elementary divisor rings in \textscCoq (2016)
- Liu, Shaoying: Testing-based formal verification for theorems and its application in software specification verification (2016)
- Maletzky, Alexander: Mathematical theory exploration in Theorema: reduction rings (2016)
- Nipkow, Tobias: Automatic functional correctness proofs for functional search trees (2016)
- Pham, Tuan-Hung; Gacek, Andrew; Whalen, Michael W.: Reasoning about algebraic data types with abstractions (2016)