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 236 articles , 1 standard article )
Showing results 1 to 20 of 236.
Sorted by year (citations)
- 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 Coq (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)
- Smith, Eric; Coglio, Alessandro: Android platform modeling and android app verification in the ACL2 theorem prover (2016) ioport
- Zhang, Nan; Duan, Zhenhua; Tian, Cong: A complete axiom system for propositional projection temporal logic with cylinder computation model (2016)
- Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)
- Bancerek, Grzegorz; Byliński, Czesław; Grabowski, Adam; Korniłowicz, Artur; Matuszewski, Roman; Naumowicz, Adam; Pąk, Karol; Urban, Josef: Mizar: state-of-the-art and beyond (2015)
- Boldo, Sylvie; Lelay, Catherine; Melquiond, Guillaume: Coquelicot: a user-friendly library of real analysis for Coq (2015)
- Davis, Jared; Myreen, Magnus O.: The reflective Milawa theorem prover is sound (down to the machine code that runs it) (2015)