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 154 articles , 1 standard article )
Showing results 1 to 20 of 154.
Sorted by year (citations)
- 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)
- Zhang, Nan; Yang, Mengfei; Gu, Bin; Duan, Zhenhua; Tian, Cong: Verifying safety critical task scheduling systems in PPTL axiom system (2016)
- 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)
- Heras, Jónathan; Martín-Mateos, Francisco Jesús; Pascual, Vico: Modelling algebraic structures and morphisms in ACL2 (2015)
- Jacobsen, Charles; Solovyev, Alexey; Gopalakrishnan, Ganesh: A parameterized floating-point formalizaton in HOL Light (2015)
- Rosén, Dan; Smallbone, Nicholas: TIP: tools for inductive provers (2015)
- Groce, Alex; Havelund, Klaus; Holzmann, Gerard; Joshi, Rajeev; Xu, Ru-Gang: Establishing flight software reliability: testing, model checking, constraint-solving, monitoring and learning (2014)
- Kaufmann, Matt; Moore, J Strother: Rough diamond: an extension of equivalence-based rewriting (2014)
- Lambán, L.; Rubio, J.; Martín-Mateos, F.J.; Ruiz-Reina, J.L.: Verifying the bridge between simplicial topology and algebra: the Eilenberg-Zilber algorithm (2014)
- Moore, J Strother: Proof pearl: proving a simple von Neumann machine Turing complete (2014)
- Myreen, Magnus O.; Davis, Jared: The reflective milawa theorem prover is sound (down to the machine code that runs it) (2014)
- Omodeo, Eugenio G.; Tomescu, Alexandru I.: Set graphs. III: Proof pearl: Claw-free graphs mirrored into transitive hereditarily finite sets (2014)
- Puri, Disha; Ray, Sandip; Hao, Kecheng; Xie, Fei: Mechanical certification of loop pipelining transformations: a preview (2014)
- Zhang, Nan; Duan, Zhenhua; Tian, Cong: An axiomatization for cylinder computation model (2014)
- Abed, Sa’ed; Mohamed, Otmane Ait; Al Sammane, Ghiath: Automatic verification of reduction techniques in higher order logic (2013)
- Boldo, Sylvie; Clément, François; Filli^atre, Jean-Christophe; Mayero, Micaela; Melquiond, Guillaume; Weis, Pierre: Wave equation numerical resolution: a comprehensive mechanized proof of a C program (2013)