A Modular Integration of SAT/SMT Solvers to Coq through Proof Witnesses (Q3100209): Difference between revisions

@@ Property / author @@
+Germain Faure
@@ Property / author: Germain Faure / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Coq
@@ Property / describes a project that uses: Coq / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+HOL Light
@@ Property / describes a project that uses: HOL Light / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+GitHub
@@ Property / describes a project that uses: GitHub / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+zChaff
@@ Property / describes a project that uses: zChaff / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+z3
@@ Property / describes a project that uses: z3 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+veriT
@@ Property / describes a project that uses: veriT / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+CVC Lite
@@ Property / describes a project that uses: CVC Lite / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+SMT-LIB
@@ Property / describes a project that uses: SMT-LIB / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1007/978-3-642-25379-9_12
+Normal rank
@@ Property / OpenAlex ID @@
+W81349459
@@ Property / OpenAlex ID: W81349459 / rank @@
+Normal rank
@@ Property / cites work @@
+Extending Coq with Imperative Features and Its Application to SAT Verification
+Normal rank
@@ Property / cites work @@
+Autarkic computations in formal proofs
@@ Property / cites work: Autarkic computations in formal proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Fast Reflexive Arithmetic Tactics the Linear Case and Beyond
+Normal rank
@@ Property / cites work @@
+Fast LCF-Style Proof Reconstruction for Z3
@@ Property / cites work: Fast LCF-Style Proof Reconstruction for Z3 / rank @@
+Normal rank
@@ Property / cites work @@
+Tools and Algorithms for the Construction and Analysis of Systems
+Normal rank
@@ Property / cites work @@
+Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
+Normal rank
@@ Property / cites work @@
+Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme
+Normal rank
@@ Property / cites work @@
+Q2848688
@@ Property / cites work: Q2848688 / rank @@
+Normal rank
@@ Property / cites work @@
+Solving SAT and SAT Modulo Theories
@@ Property / cites work: Solving SAT and SAT Modulo Theories / rank @@
+Normal rank