Formal Verification of Bit-Vector Invertibility Conditions in Coq (Q6496617): Difference between revisions

@@ Property / cites work @@
+Theorem Proving in Higher Order Logics
@@ Property / cites work: Theorem Proving in Higher Order Logics / rank @@
+Normal rank
@@ Property / cites work @@
+From Sets to Bits in Coq
@@ Property / cites work: From Sets to Bits in Coq / rank @@
+Normal rank
@@ Property / cites work @@
+Hammer for Coq: automation for dependent type theory
+Normal rank
@@ Property / cites work @@
+Q2767010
@@ Property / cites work: Q2767010 / rank @@
+Normal rank
@@ Property / cites work @@
+SMTCoq: a plug-in for integrating SMT solvers into Coq
+Normal rank
@@ Property / cites work @@
+Solving quantified bit-vectors using invertibility conditions
+Normal rank
@@ Property / cites work @@
+Towards satisfiability modulo parametric bit-vectors
+Normal rank
@@ Property / cites work @@
+Towards bit-width-independent proofs in SMT solvers
+Normal rank
@@ Property / cites work @@
+Q4281483
@@ Property / cites work: Q4281483 / rank @@
+Normal rank
@@ Property / cites work @@
+Q5219927
@@ Property / cites work: Q5219927 / rank @@
+Normal rank
@@ Property / cites work @@
+CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
+Normal rank
@@ Property / cites work @@
+Equations: A Dependent Pattern-Matching Compiler
@@ Property / cites work: Equations: A Dependent Pattern-Matching Compiler / rank @@
+Normal rank