Clark Barrett, Aaron Stump & Cesare Tinelli (2010):
The SMT-LIB Standard: Version 2.0.
In: A. Gupta & D. Kroening: Proceedings of the 8th International Workshop on Satisfiability Modulo Theories (Edinburgh, UK).
Arthur Blot, Pierre-Evariste Dagand & Julia Lawall:
Bit Sequences and Bit Sets Library.
Available at https://github.com/pedagand/ssrbit.
Tej Chajed, Haogang Chen, Adam Chlipala, Joonwon Choi, Andres Erbsen, Jason Gross, Samuel Gruetter, Frans Kaashoek, Alex Konradi, Gregory Malecha, Duckki Oe, Murali Vijayaraghavan, Nickolai Zeldovich & Daniel Ziegler:
Bedrock Bit Vectors Library.
Available at https://github.com/mit-plv/bbv.
Lukasz Czajka & Cezary Kaliszyk (2018):
Hammer for Coq: Automation for Dependent Type Theory.
J. Autom. Reasoning 61(1-4),
pp. 423–453,
doi:10.1007/s10817-018-9458-4.
Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds & Clark Barrett (2017):
SMTCoq: A Plug-In for Integrating SMT Solvers into Coq.
In: Proceedings of 29th International Conference on Computer Aided Verification (CAV 2017),
Lecture Notes in Computer Science 10427.
Springer,
pp. 126–133,
doi:10.1007/s10703-012-0163-3.
Herbert B. Enderton (2001):
Chapter TWO - First-Order Logic.
In: Herbert B. Enderton: A Mathematical Introduction to Logic (Second Edition),
second edition edition.
Academic Press,
Boston,
pp. 67 – 181,
doi:10.1016/B978-0-08-049646-7.50008-4.
Aarti Gupta & Allan L. Fisher (1993):
Representation and Symbolic Manipulation of Linearly Inductive Boolean Functions.
In: Proceedings of the 1993 IEEE/ACM International Conference on Computer-aided Design,
ICCAD '93.
IEEE Computer Society Press,
Los Alamitos, CA, USA,
pp. 192–199.
Available at http://dl.acm.org.stanford.idm.oclc.org/citation.cfm?id=259794.259827.
Aina Niemetz, Mathias Preiner, Andrew Reynolds, Clark Barrett & Cesare Tinelli (2018):
Solving Quantified Bit-Vectors Using Invertibility Conditions.
In: Proceedings of 30th International Conference on Computer Aided Verification (CAV 2018),
pp. 236–255,
doi:10.1007/978-3-319-96142-2_16.
Aina Niemetz, Mathias Preiner, Andrew Reynolds Yoni Zohar, Clark Barrett & Cesare Tinelli (2019):
Towards Bit-Width-Independent Proofs in SMT Solvers.
To appear in the proceedings of CADE-27.
Tobias Nipkow, Lawrence C Paulson & Markus Wenzel (2002):
Isabelle/HOL: a proof assistant for higher-order logic.
Lecture Notes in Computer Science 2283.
Springer Science & Business Media,
doi:10.1007/3-540-45949-9_6.
Matthieu Sozeau (2010):
Equations: A Dependent Pattern-Matching Compiler.
In: Proceedings of the 1st International Conference on Interactive Theorem Proving (ITP 2010),
pp. 419–434,
doi:10.1007/978-3-642-14052-5_29.
eptcs@eptcs.org